(*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * This software may be distributed and modified according to the terms of
 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
 * See "LICENSE_GPLv2.txt" for details.
 *
 * @TAG(GD_GPL)
 *)

theory Tcb_C
imports Move Delete_C
begin

lemma asUser_obj_at' :
  " \<lbrace> K(t\<noteq>t') and obj_at' P t' \<rbrace> asUser t f \<lbrace> \<lambda>_.  obj_at' (P::Structures_H.tcb \<Rightarrow> bool) t' \<rbrace>"
  apply (simp add: asUser_def )
  apply wp
  apply (simp add: split_def)
  apply (wp threadSet_obj_at') 
  apply (case_tac "t=t'")
   apply clarsimp
  apply clarsimp
  apply (rule hoare_drop_imps)+
  apply wp
done


lemma getObject_sched:
  "(x::tcb, s') \<in> fst (getObject t s) \<Longrightarrow>
  (x,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (getObject t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))"
  apply (clarsimp simp: in_monad getObject_def split_def loadObject_default_def 
                        magnitudeCheck_def projectKOs
                  split: option.splits)
  done

lemma threadGet_sched:
  "(x, s') \<in> fst (threadGet t f s) \<Longrightarrow>
  (x,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (threadGet t f (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))"
  apply (clarsimp simp: in_monad threadGet_def liftM_def)
  apply (drule getObject_sched)
  apply fastforce
  done

lemma setObject_sched:
  "(x, s') \<in> fst (setObject t (v::tcb) s) \<Longrightarrow>
  (x, s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (setObject t v (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))"
  apply (clarsimp simp: in_monad setObject_def split_def updateObject_default_def
                        magnitudeCheck_def projectKOs
                  split: option.splits)
  done

lemma threadSet_sched:
  "(x, s') \<in> fst (threadSet f t s) \<Longrightarrow>
  (x,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (threadSet f t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))"
  apply (clarsimp simp: in_monad threadSet_def)
  apply (drule getObject_sched)
  apply (drule setObject_sched)
  apply fastforce
  done

lemma asUser_sched:
  "(rv,s') \<in> fst (asUser t f s) \<Longrightarrow>
  (rv,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (asUser t f (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))"
  apply (clarsimp simp: asUser_def split_def in_monad select_f_def)
  apply (drule threadGet_sched)
  apply (drule threadSet_sched)
  apply fastforce
  done

lemma doMachineOp_sched:
  "(rv,s') \<in> fst (doMachineOp f s) \<Longrightarrow>
  (rv,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (doMachineOp f (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))"
  apply (clarsimp simp: doMachineOp_def split_def in_monad select_f_def)
  apply fastforce
  done

crunch queues[wp]: setupReplyMaster "valid_queues"
  (simp: crunch_simps wp: crunch_wps)

crunch curThread [wp]: restart "\<lambda>s. P (ksCurThread s)"
  (wp: crunch_wps simp: crunch_simps)

context kernel_m
begin

lemma getMRs_rel_sched:
  "\<lbrakk> getMRs_rel args buffer s;
     (cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer) s \<rbrakk>
  \<Longrightarrow> getMRs_rel args buffer (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)"
  apply (clarsimp simp: getMRs_rel_def)
  apply (rule exI, rule conjI, assumption)
  apply (subst det_wp_use, rule det_wp_getMRs)
   apply (simp add: cur_tcb'_def split: option.splits)
   apply (simp add: valid_ipc_buffer_ptr'_def)
  apply (subst (asm) det_wp_use, rule det_wp_getMRs)
   apply (simp add: cur_tcb'_def)
  apply (clarsimp simp: getMRs_def in_monad)
  apply (drule asUser_sched)
  apply (intro exI)
  apply (erule conjI)
  apply (cases buffer)
   apply (simp add: return_def)
  apply clarsimp
  apply (drule mapM_upd [rotated])
   prefer 2
   apply fastforce
  apply (clarsimp simp: loadWordUser_def in_monad stateAssert_def word_size)
  apply (erule doMachineOp_sched)
  done

lemma getObject_state:
  " \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk>
  \<Longrightarrow> (if t = t' then tcbState_update (\<lambda>_. st) x else x, 
      s'\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)
      \<in> fst (getObject t' (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>))"
  apply (simp split: split_if)
  apply (rule conjI)
   apply clarsimp
   apply (clarsimp simp: getObject_def split_def loadObject_default_def in_monad 
                         Corres_C.in_magnitude_check' projectKOs objBits_simps)
   apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs objBits_simps)
   apply (simp add: magnitudeCheck_def in_monad split: option.splits)
   apply clarsimp
   apply (simp add: lookupAround2_char2)
   apply (clarsimp split: split_if_asm)
   apply (erule_tac x=x2 in allE)
   apply (clarsimp simp: ps_clear_def)
   apply (drule_tac x=x2 in orthD2)
    apply fastforce
   apply clarsimp
   apply (erule impE) 
    apply simp
   apply (erule notE, rule word_diff_ls'(3))
    apply unat_arith
   apply (drule is_aligned_no_overflow, simp add: word_bits_def)
  apply clarsimp
  apply (clarsimp simp: getObject_def split_def loadObject_default_def in_monad 
                        Corres_C.in_magnitude_check' projectKOs objBits_simps)
  apply (simp add: magnitudeCheck_def in_monad split: option.splits)
  apply clarsimp
  apply (simp add: lookupAround2_char2)
  apply (clarsimp split: split_if_asm)
   apply (erule_tac x=t in allE)
   apply simp
   apply (clarsimp simp: obj_at'_real_def projectKOs 
                         ko_wp_at'_def objBits_simps)
   apply (simp add: ps_clear_def)
   apply (drule_tac x=t in orthD2)
    apply fastforce
   apply clarsimp
   apply (erule impE)
    apply simp
   apply (erule notE, rule word_diff_ls'(3))
    apply unat_arith
   apply (drule is_aligned_no_overflow)
   apply simp
  apply (erule_tac x=x2 in allE)
  apply (clarsimp simp: ps_clear_def)
  apply (drule_tac x=x2 in orthD2)
   apply fastforce
  apply clarsimp
  apply (erule impE)
   apply (rule word_diff_ls'(3))
   apply unat_arith
   apply (drule is_aligned_no_overflow)
   apply simp
  apply fastforce
  done


lemma threadGet_state:
  "\<lbrakk> (uc, s') \<in> fst (threadGet tcbContext t' s); ko_at' ko t s \<rbrakk> \<Longrightarrow>
   (uc, s'\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> 
  fst (threadGet tcbContext t' (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>))"
  apply (clarsimp simp: threadGet_def liftM_def in_monad)
  apply (drule (1) getObject_state [where st=st])   
  apply (rule exI)
  apply (erule conjI)
  apply (simp split: if_splits)
  done

lemma asUser_state:
  "\<lbrakk>(x,s) \<in> fst (asUser t' f s); ko_at' ko t s; \<And>s. \<lbrace>op = s\<rbrace> f \<lbrace>\<lambda>_. op = s\<rbrace> \<rbrakk> \<Longrightarrow>
  (x,s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> 
  fst (asUser t' f (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>))"
  apply (clarsimp simp: asUser_def in_monad select_f_def)
  apply (frule use_valid, rule threadGet_inv [where P="op = s"], rule refl)
  apply (frule use_valid, assumption, rule refl)
  apply clarsimp
  apply (frule (1) threadGet_state)
  apply (intro exI)
  apply (erule conjI)
  apply (rule exI, erule conjI)
  apply (clarsimp simp: threadSet_def in_monad)
  apply (frule use_valid, rule getObject_inv [where P="op = s"])
    apply (simp add: loadObject_default_def)
    apply wp
    apply simp
   apply (rule refl)
  apply clarsimp
  apply (frule (1) getObject_state)
  apply (intro exI)
  apply (erule conjI)
  apply (clarsimp simp: setObject_def split_def updateObject_default_def threadGet_def
                        in_magnitude_check' getObject_def loadObject_default_def liftM_def
                        objBits_simps projectKOs in_monad)
  apply (simp split: split_if)
  apply (rule conjI)
   apply (clarsimp simp: obj_at'_def projectKOs objBits_simps)
   apply (clarsimp simp: magnitudeCheck_def in_monad split: option.splits)
   apply (rule conjI)
    apply clarsimp
    apply (cases s, simp)
    apply (rule ext)
    apply (clarsimp split: split_if)
    apply (cases ko)
    apply clarsimp
   apply clarsimp
   apply (rule conjI)
    apply (clarsimp simp add: lookupAround2_char2 split: split_if_asm)
    apply (erule_tac x=x2 in allE)
    apply simp
    apply (simp add: ps_clear_def)
    apply (drule_tac x=x2 in orthD2)
     apply fastforce
    apply clarsimp
    apply (erule impE, simp)
    apply (erule notE, rule word_diff_ls'(3))
     apply unat_arith
    apply (drule is_aligned_no_overflow)
    apply simp
   apply (rule exI)
   apply (rule conjI, fastforce)
   apply clarsimp
   apply (cases s, clarsimp)
   apply (rule ext, clarsimp split: split_if)
   apply (cases ko, clarsimp)
  apply (clarsimp simp: magnitudeCheck_def in_monad split: option.splits)
  apply (rule conjI)
   apply clarsimp
   apply (cases s, clarsimp)
   apply (rule ext, clarsimp split: split_if)
   apply (case_tac tcb, clarsimp)
  apply clarsimp
  apply (rule conjI)
   apply (clarsimp simp add: lookupAround2_char2 split: split_if_asm)
    apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs objBits_simps)
    apply (erule_tac x=t in allE)
    apply simp
    apply (simp add: ps_clear_def)
    apply (drule_tac x=t in orthD2)
     apply fastforce
    apply clarsimp
    apply (erule impE, simp)
    apply (erule notE, rule word_diff_ls'(3))
     apply unat_arith
    apply (drule is_aligned_no_overflow)
    apply simp
   apply (erule_tac x=x2 in allE)
   apply simp
   apply (simp add: ps_clear_def)
   apply (drule_tac x=x2 in orthD2)
    apply fastforce
   apply clarsimp
   apply (erule impE)
    apply (rule word_diff_ls'(3))
     apply unat_arith
    apply (drule is_aligned_no_overflow)
    apply simp
   apply (erule impE, simp)
   apply simp
  apply (rule exI)
  apply (rule conjI, fastforce)
  apply clarsimp
  apply (cases s, clarsimp)
  apply (rule ext, clarsimp split: split_if)
  apply (case_tac tcb, clarsimp)
  done

lemma doMachineOp_state:
  "(rv,s') \<in> fst (doMachineOp f s) \<Longrightarrow>
  (rv,s'\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)
  \<in> fst (doMachineOp f (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>))"
  apply (clarsimp simp: doMachineOp_def split_def in_monad select_f_def)
  apply fastforce
  done

lemma mapM_upd_inv:
  assumes f: "\<And>x rv. (rv,s) \<in> fst (f x s) \<Longrightarrow> x \<in> set xs \<Longrightarrow> (rv, g s) \<in> fst (f x (g s))"
  assumes inv: "\<And>x. \<lbrace>op = s\<rbrace> f x \<lbrace>\<lambda>_. op = s\<rbrace>"
  shows "(rv,s) \<in> fst (mapM f xs s) \<Longrightarrow> (rv, g s) \<in> fst (mapM f xs (g s))"
  using f inv
proof (induct xs arbitrary: rv s)
  case Nil
  thus ?case by (simp add: mapM_Nil return_def)
next
  case (Cons z zs)
  from Cons.prems
  show ?case
    apply (clarsimp simp: mapM_Cons in_monad)
    apply (frule use_valid, assumption, rule refl)
    apply clarsimp
    apply (drule Cons.prems, simp)
    apply (rule exI, erule conjI)
    apply (drule Cons.hyps)
      apply simp
     apply assumption
    apply simp
    done
qed 

lemma getMRs_rel_state:
  "\<lbrakk>getMRs_rel args buffer s; 
    (cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer) s;
    ko_at' ko t s \<rbrakk> \<Longrightarrow>
  getMRs_rel args buffer (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)"
  apply (clarsimp simp: getMRs_rel_def)
  apply (rule exI, erule conjI)
  apply (subst (asm) det_wp_use, rule det_wp_getMRs)
   apply (simp add: cur_tcb'_def)
  apply (subst det_wp_use, rule det_wp_getMRs)
   apply (simp add: cur_tcb'_def)
   apply (rule conjI)
    apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs 
                          objBits_simps ps_clear_def split: split_if)
   apply (clarsimp simp: valid_ipc_buffer_ptr'_def split: option.splits)
   apply (clarsimp simp: typ_at'_def ko_wp_at'_def projectKOs obj_at'_real_def
                         objBits_simps ps_clear_def split: split_if)
  apply (clarsimp simp: getMRs_def in_monad)
  apply (frule use_valid, rule asUser_inv [where P="op = s"])
    apply (wp mapM_wp' getRegister_inv)[1]
   apply simp
  apply clarsimp
  apply (drule (1) asUser_state)
   apply (wp mapM_wp' getRegister_inv)[1]
  apply (intro exI)
  apply (erule conjI)
  apply (cases buffer)
   apply (clarsimp simp: return_def)
  apply clarsimp 
  apply (drule mapM_upd_inv [rotated -1]) 
    prefer 3
    apply fastforce
   prefer 2
   apply wp
  apply (clarsimp simp: loadWordUser_def in_monad stateAssert_def word_size
                  simp del: fun_upd_apply)
  apply (rule conjI)
   apply (clarsimp simp: pointerInUserData_def typ_at'_def ko_wp_at'_def 
                         projectKOs ps_clear_def obj_at'_real_def
                  split: split_if)
  apply (erule doMachineOp_state)
  done

lemma setTCB_cur:
  "\<lbrace>cur_tcb'\<rbrace> setObject t (v::tcb) \<lbrace>\<lambda>_. cur_tcb'\<rbrace>"
  apply (wp cur_tcb_lift)
  apply (simp add: setObject_def split_def updateObject_default_def)
  apply wp
  apply simp
  done

lemma setThreadState_getMRs_rel:
  "\<lbrace>getMRs_rel args buffer and cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer
           and (\<lambda>_. runnable' st)\<rbrace> 
      setThreadState st t \<lbrace>\<lambda>_. getMRs_rel args buffer\<rbrace>"
  apply (rule hoare_gen_asm')
  apply (simp add: setThreadState_runnable_simp)
  apply (simp add: threadSet_def)
  apply wp
   apply (simp add: setObject_def split_def updateObject_default_def)
   apply wp
  apply (simp del: fun_upd_apply)
  apply (wp getObject_tcb_wp)
  apply (clarsimp simp del: fun_upd_apply)
  apply (drule obj_at_ko_at')+
  apply (clarsimp simp del: fun_upd_apply)
  apply (rule exI, rule conjI, assumption)
  apply (clarsimp split: split_if simp del: fun_upd_apply)
  apply (simp add: getMRs_rel_state)
  done

lemma setThreadState_sysargs_rel:
  "\<lbrace>sysargs_rel args buffer and (\<lambda>_. runnable' st)\<rbrace> setThreadState st t \<lbrace>\<lambda>_. sysargs_rel args buffer\<rbrace>" 
  apply (cases buffer, simp_all add: sysargs_rel_def)
   apply (rule hoare_pre)
   apply (wp setThreadState_getMRs_rel hoare_valid_ipc_buffer_ptr_typ_at'|simp)+
  done

lemma ccorres_abstract_known:
  "\<lbrakk> \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val) \<rbrakk> 
     \<Longrightarrow> ccorres rvr xf P (P' \<inter> {s. xf' s = val}) hs f g"
  apply (rule ccorres_guard_imp2)
   apply (rule_tac xf'=xf' in ccorres_abstract)
    apply assumption
   apply (rule_tac P="rv' = val" in ccorres_gen_asm2)
   apply simp
  apply simp
  done

lemma distinct_remove1_filter:
  "distinct xs \<Longrightarrow> remove1 v xs = [x\<leftarrow>xs. x \<noteq> v]"
  apply (induct xs)
   apply simp
  apply (clarsimp split: split_if)
  apply (rule sym, simp add: filter_id_conv)
  apply clarsimp
  done

lemma hrs_mem_update_cong:
  "\<lbrakk> \<And>x. f x = f' x \<rbrakk> \<Longrightarrow> hrs_mem_update f = hrs_mem_update f'"
  by (simp add: hrs_mem_update_def)

lemma setPriority_ccorres:
  "ccorres dc xfdc
      (invs' and tcb_at' t and (\<lambda>s. priority \<le> maxPriority))
      (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr t} \<inter> {s. prio_' s = ucast priority})
      [] (setPriority t priority) (Call setPriority_'proc)"
  apply (rule ccorres_gen_asm)
  apply (cinit lift: tptr_' prio_')
   apply (ctac(no_vcg) add: tcbSchedDequeue_ccorres)
    apply (rule ccorres_move_c_guard_tcb)
    apply (rule ccorres_split_nothrow_novcg_dc)
       apply (rule threadSet_ccorres_lemma2[where P=\<top>])
        apply vcg
       apply clarsimp
       apply (erule(1) rf_sr_tcb_update_no_queue2,
              (simp add: typ_heap_simps)+, simp_all)[1]
         apply (subst heap_update_field_hrs | fastforce intro: typ_heap_simps)+
        apply (rule ball_tcb_cte_casesI, simp+)
       apply (simp add: ctcb_relation_def cast_simps)
       apply (clarsimp simp: down_cast_same [symmetric] ucast_up_ucast is_up is_down)
      apply (ctac(no_vcg) add: isRunnable_ccorres)
       apply (rule ccorres_split_nothrow_novcg_dc)
          apply (simp add: when_def to_bool_def del: Collect_const)
          apply (rule ccorres_cond2[where R=\<top>], simp add: Collect_const_mem)
           apply (ctac add: tcbSchedEnqueue_ccorres)
          apply (rule ccorres_return_Skip)
         apply (rule ccorres_pre_getCurThread)
         apply (simp add: when_def to_bool_def)
         apply (rule_tac R="\<lambda>s. rvb = ksCurThread s"
                    in ccorres_cond2)
           apply (clarsimp simp: rf_sr_ksCurThread)
          apply (ctac add: rescheduleRequired_ccorres[unfolded dc_def])
         apply (rule ccorres_return_Skip')
        apply simp
        apply (wp hoare_drop_imps weak_sch_act_wf_lift_linear)
       apply (simp add: guard_is_UNIV_def)
      apply simp
      apply wp
     apply simp
     apply (rule_tac Q="\<lambda>rv s. valid_queues s \<and> valid_objs' s \<and> tcb_at' t s
                  \<and> weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp)
      apply (clarsimp simp: st_tcb_at'_def o_def valid_objs'_maxDomain
                            valid_objs'_maxPriority
                     split: if_splits)
     apply (wp hoare_drop_imps threadSet_valid_queues threadSet_valid_objs'
               weak_sch_act_wf_lift_linear threadSet_st_tcb_at_state)
      apply (clarsimp simp: st_tcb_at'_def o_def split: if_splits)
     apply (wp threadSet_tcbDomain_triv)
     apply simp
    apply (simp add: guard_is_UNIV_def)
   apply (simp add: inQ_def pred_conj_def conj_comms)
   apply (wp weak_sch_act_wf_lift_linear)
    apply (rule hoare_strengthen_post,
          rule tcbSchedDequeue_nonq[where t'=t])
   apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def)
   apply (fastforce simp: invs'_def valid_state'_def
                          valid_objs'_maxDomain valid_objs'_maxPriority)
  done

lemma ccorres_subgoal_tailE:
  "\<lbrakk> ccorres rvr xf Q Q' hs (b ()) d;
      ccorres rvr xf Q Q' hs (b ()) d \<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c ;; d) \<rbrakk>
        \<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c ;; d)"
  by simp

lemma checkCapAt_ccorres:
  "\<lbrakk> \<And>rv' t t'. ceqv \<Gamma> ret__unsigned_long_' rv' t t' c (c' rv');
      ccorres rvr xf P P' hs (f >>= g) (c' (scast true));
      ccorres rvr xf Q Q' hs (g ()) (c' (scast false));
      guard_is_UNIV dc xfdc (\<lambda>_ _. P' \<inter> Q') \<rbrakk>
    \<Longrightarrow> ccorres rvr xf (invs' and valid_cap' cap and P and Q)
                       (UNIV \<inter> {s. ccap_relation cap cap'} \<inter> {s. slot' = cte_Ptr slot}) hs
         (checkCapAt cap slot f >>= g)
         (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t slot'\<rbrace>
            (\<acute>ret__unsigned_long :== CALL sameObjectAs(cap',
                h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot'\<rightarrow>[''cap_C'']))));;c)"
  apply (rule ccorres_gen_asm2)+
  apply (simp add: checkCapAt_def liftM_def bind_assoc del: Collect_const)
  apply (rule ccorres_symb_exec_l' [OF _ getCTE_inv getCTE_sp empty_fail_getCTE])
  apply (rule ccorres_guard_imp2)
   apply (rule ccorres_move_c_guard_cte)
   apply (rule_tac xf'=ret__unsigned_long_' and val="from_bool (sameObjectAs cap (cteCap x))"
                and R="cte_wp_at' (op = x) slot and valid_cap' cap and invs'"
                 in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV])
      apply vcg
      apply (clarsimp simp: cte_wp_at_ctes_of)
      apply (erule(1) cmap_relationE1[OF cmap_relation_cte])
      apply (rule exI, rule conjI, assumption)
      apply (clarsimp simp: typ_heap_simps dest!: ccte_relation_ccap_relation)
      apply (rule exI, rule conjI, assumption)
      apply (auto intro: valid_capAligned dest: ctes_of_valid')[1]
     apply assumption
    apply (simp only: when_def if_to_top_of_bind)
    apply (rule ccorres_if_lhs)
     apply (simp add: from_bool_def true_def)
    apply (simp add: from_bool_def false_def)
   apply (simp add: guard_is_UNIV_def)
  apply (clarsimp simp: cte_wp_at_ctes_of)
  done

lemmas checkCapAt_ccorres2
    = checkCapAt_ccorres[where g=return, simplified bind_return]

lemma invs_psp_aligned_strg':
  "invs' s \<longrightarrow> pspace_aligned' s"
  by clarsimp

lemma cte_is_derived_capMasterCap_strg:
  "cte_wp_at' (is_derived' (ctes_of s) ptr cap \<circ> cteCap) ptr s
    \<longrightarrow> cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap \<or> P) ptr s"
  by (clarsimp simp: cte_wp_at_ctes_of is_derived'_def
                     badge_derived'_def)

lemma cteInsert_cap_to'2:
  "\<lbrace>ex_nonz_cap_to' p\<rbrace>
     cteInsert newCap srcSlot destSlot
   \<lbrace>\<lambda>_. ex_nonz_cap_to' p\<rbrace>"
  apply (simp add: cteInsert_def ex_nonz_cap_to'_def setUntypedCapAsFull_def)
  apply (rule hoare_vcg_ex_lift)
  apply (wp updateMDB_weak_cte_wp_at
            updateCap_cte_wp_at_cases getCTE_wp' static_imp_wp)
  apply (clarsimp simp: cte_wp_at_ctes_of)
  apply auto
  done

lemma invokeTCB_ThreadControl_ccorres:
  "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_')
   (invs' and sch_act_simple 
          and tcb_inv_wf' (ThreadControl target slot faultep priority cRoot vRoot buf)
          and (\<lambda>_. (faultep = None) = (cRoot = None) \<and> (cRoot = None) = (vRoot = None)
                    \<and> (case buf of Some (ptr, Some (cap, slot)) \<Rightarrow> slot \<noteq> 0 | _ \<Rightarrow> True)))
   (UNIV \<inter> {s. target_' s = tcb_ptr_to_ctcb_ptr target}
         \<inter> {s. (cRoot \<noteq> None \<or> buf \<noteq> None) \<longrightarrow> slot_' s = cte_Ptr slot}
         \<inter> {s. faultep_' s = option_to_0 faultep}
         \<inter> {s. priority_' s = case_option 0 ucast priority}
         \<inter> {s. case cRoot of None \<Rightarrow> True | Some (cRootCap, cRootSlot) \<Rightarrow> ccap_relation cRootCap (cRoot_newCap_' s)}
         \<inter> {s. cRoot_srcSlot_' s = cte_Ptr (option_to_0 (option_map snd cRoot))}
         \<inter> {s. case vRoot of None \<Rightarrow> True | Some (vRootCap, vRootSlot) \<Rightarrow> ccap_relation vRootCap (vRoot_newCap_' s)}
         \<inter> {s. vRoot_srcSlot_' s = cte_Ptr (option_to_0 (option_map snd vRoot))}
         \<inter> {s. bufferAddr_' s = option_to_0 (option_map fst buf)}
         \<inter> {s. bufferSrcSlot_' s = cte_Ptr (case buf of Some (ptr, Some (cap, slot)) \<Rightarrow> slot | _ \<Rightarrow> 0)}
         \<inter> {s. case buf of Some (ptr, Some (cap, slot)) \<Rightarrow> ccap_relation cap (bufferCap_' s) | _ \<Rightarrow> True}
         \<inter> {s. updateFlags_' s = (if priority \<noteq> None then scast thread_control_update_priority else 0)
                                  || (if buf \<noteq> None then scast thread_control_update_ipc_buffer else 0)
                                  || (if cRoot \<noteq> None then scast thread_control_update_space else 0)})
   []
   (invokeTCB (ThreadControl target slot faultep priority cRoot vRoot buf))
   (Call invokeTCB_ThreadControl_'proc)"
  (is "ccorres ?rvr ?xf (?P and (\<lambda>_. ?P')) ?Q [] ?af ?cf")
  apply (rule ccorres_gen_asm)
  apply (cinit lift: target_' slot_' faultep_' priority_' cRoot_newCap_' cRoot_srcSlot_'
                     vRoot_newCap_' vRoot_srcSlot_' bufferAddr_' bufferSrcSlot_' bufferCap_'
                     updateFlags_')
   apply csymbr
   apply (simp add: liftE_bindE case_option_If2 thread_control_flag_defs
                    word_ao_dist if_and_helper if_n_0_0
               del: Collect_const cong: call_ignore_cong if_cong)
   apply (rule_tac P="ptr_val (tcb_ptr_to_ctcb_ptr target) && ~~ mask 4
                          = ptr_val (tcb_ptr_to_ctcb_ptr target)
                        \<and> ptr_val (tcb_ptr_to_ctcb_ptr target) && 0xFFFFFE00 = target"
                in ccorres_gen_asm)
   apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow_novcg)
       apply (rule ccorres_cond_both'[where Q=\<top> and Q'=\<top>])
         apply (simp add: Collect_const_mem)
        apply (rule ccorres_move_c_guard_tcb)
        apply (rule threadSet_ccorres_lemma2[where P=\<top>])
         apply vcg
        apply clarsimp
        apply (subst StateSpace.state.fold_congs[OF refl refl])
         apply (rule globals.fold_congs[OF refl refl])
         apply (rule heap_update_field_hrs)
           apply (simp add: typ_heap_simps)
          apply (fastforce intro: typ_heap_simps)
         apply simp
        apply (erule(1) rf_sr_tcb_update_no_queue2,
               (simp add: typ_heap_simps)+)
         apply (rule ball_tcb_cte_casesI, simp+)
        apply (clarsimp simp: ctcb_relation_def option_to_0_def)
       apply (rule ccorres_return_Skip)
      apply (rule ceqv_refl)
     apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow_novcg)
         apply (rule ccorres_cond_both'[where Q=\<top> and Q'=\<top>])
           apply (simp add: Collect_const_mem)
          apply (ctac add: setPriority_ccorres)
         apply (rule ccorres_return_Skip)
        apply (rule ceqv_refl)
       apply (rule ccorres_subgoal_tailE)
        apply (rule ccorres_subgoal_tailE)
         apply (rule_tac A="invs' and sch_act_simple and tcb_at' target
                          and case_option \<top> (case_option \<top> (valid_cap' \<circ> fst) \<circ> snd) buf
                          and case_option \<top> (case_option \<top> (cte_at' \<circ> snd) \<circ> snd) buf
                          and K (case_option True (swp is_aligned msg_align_bits \<circ> fst) buf)
                          and K (case_option True (case_option True (isArchObjectCap \<circ> fst) \<circ> snd) buf)"
                           (* bits of tcb_inv_wf' *)
                     in ccorres_guard_imp2[where A'=UNIV])
          apply (rule ccorres_Cond_rhs_Seq)
           apply (simp only: if_True split_def bindE_assoc)
           apply (rule ccorres_rhs_assoc)+
           apply csymbr
           apply (rule ccorres_Guard_Seq)+
           apply csymbr
           apply (simp add: liftE_bindE[symmetric] bindE_assoc
                            getThreadBufferSlot_def
                            locateSlot_conv o_def
                       del: Collect_const)
           apply (simp add: liftE_bindE
                       del: Collect_const)
           apply (ctac(no_vcg) add: cteDelete_ccorres)
             apply (simp del: Collect_const add: Collect_False)
             apply (rule ccorres_move_c_guard_tcb)
             apply (rule ccorres_split_nothrow_novcg)
                 apply (rule threadSet_ccorres_lemma2[where P=\<top>])
                  apply vcg
                 apply clarsimp
                 apply (erule(1) rf_sr_tcb_update_no_queue2,
                        (simp add: typ_heap_simps)+, simp_all)[1]
                   apply (subst heap_update_field_hrs
                           | simp add: typ_heap_simps
                           | fastforce intro: typ_heap_simps)+
                  apply (rule ball_tcb_cte_casesI, simp+)
                 apply (clarsimp simp: ctcb_relation_def option_to_0_def)
                apply (rule ceqv_refl)
               apply csymbr
               apply (simp add: ccorres_cond_iffs Collect_False
                                split_def
                           del: Collect_const)
               apply (simp only: if_1_0_0 simp_thms)
               apply (rule ccorres_Cond_rhs_Seq)
                apply (rule ccorres_rhs_assoc)+
                apply (simp add: case_option_If2 if_n_0_0 split_def
                            del: Collect_const)
                apply (rule checkCapAt_ccorres)
                   apply ceqv
                  apply csymbr
                  apply (simp add: if_1_0_0 true_def Collect_True
                              del: Collect_const)
                  apply (rule ccorres_rhs_assoc)+
                  apply (rule checkCapAt_ccorres)
                     apply ceqv 
                    apply csymbr
                    apply (simp add: if_1_0_0 true_def Collect_True
                                del: Collect_const)
                    apply (simp add: assertDerived_def bind_assoc del: Collect_const)
                    apply (rule ccorres_symb_exec_l)
                       apply (ctac(no_vcg) add: cteInsert_ccorres)
                        apply (rule ccorres_return_CE, simp+)[1]
                       apply (wp empty_fail_stateAssert | simp)+
                   apply csymbr
                   apply (simp add: if_1_0_0 Collect_False false_def
                               del: Collect_const)
                   apply (rule ccorres_return_CE, simp+)[1]
                  apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem
                                        tcb_ptr_to_ctcb_ptr_mask tcbBuffer_def
                                        size_of_def cte_level_bits_def
                                        tcbIPCBufferSlot_def)
                 apply csymbr
                 apply (simp add: if_1_0_0 false_def)
                 apply (rule ccorres_cond_false_seq, simp)
                 apply (rule ccorres_return_CE, simp+)[1]
                apply (simp add: guard_is_UNIV_def if_1_0_0 false_def
                                 Collect_const_mem)
                apply (clarsimp simp: ccap_relation_def cap_thread_cap_lift
                                      cap_to_H_def)
               apply (rule ccorres_cond_false_seq | simp)+
               apply (simp split: option.split_asm)
               apply (rule ccorres_return_CE, simp+)[1]
              apply simp
              apply (rule_tac P="is_aligned (fst (the buf)) msg_align_bits"
                           in hoare_gen_asm)
              apply (strengthen cte_is_derived_capMasterCap_strg
                     impI[OF invs_valid_objs'] impI[OF invs_mdb'] impI[OF invs_pspace_aligned'],
                     simp add: o_def)
                apply (wp threadSet_ipcbuffer_trivial static_imp_wp | simp )+
                apply (wp hoare_drop_imp)
                apply (wp threadSet_ipcbuffer_trivial | simp)+
             apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem
                                   word_sle_def tcbBuffer_def size_of_def
                                   tcbIPCBufferSlot_def from_bool_def true_def
                                   cte_level_bits_def
                            split: option.split_asm)
            apply simp
            apply (rule ccorres_split_throws)
             apply (rule ccorres_return_C_errorE, simp+)[1]
            apply vcg
           apply (simp add: conj_comms cong: conj_cong)
           apply (wp hoare_vcg_const_imp_lift_R cteDelete_invs')
          apply simp
          apply (rule ccorres_return_CE)
            apply (simp+)[3]
         apply (clarsimp simp: inQ_def Collect_const_mem cintr_def
                               exception_defs)
         apply (simp add: tcbBuffer_def tcbIPCBufferSlot_def word_sle_def
                          cte_level_bits_def from_bool_def true_def size_of_def)
         apply (clarsimp simp: case_option_If2 if_n_0_0)
         apply (simp add: valid_cap'_def capAligned_def)
         apply (clarsimp simp: objBits_simps word_bits_conv
                               obj_at'_def projectKOs)
        apply (rule ccorres_Cond_rhs_Seq)
         apply (rule ccorres_rhs_assoc)+
         apply csymbr
         apply (rule ccorres_Guard_Seq)+
         apply (simp add: split_def getThreadVSpaceRoot_def locateSlot_conv
                          bindE_assoc
                     del: Collect_const)
         apply csymbr
         apply (ctac(no_vcg) add: cteDelete_ccorres)
           apply (simp add: liftE_bindE Collect_False ccorres_cond_iffs
                            dc_def
                       del: Collect_const)
           apply ((rule ccorres_split_nothrow_novcg_dc[rotated], assumption)
                   | rule ccorres_rhs_assoc2)+
             apply (simp add: conj_comms pred_conj_def)
             apply (simp add: o_def cong: conj_cong option.case_cong)

             apply (wp checked_insert_tcb_invs' hoare_case_option_wp
                       checkCap_inv [where P="tcb_at' p0" for p0]
                       checkCap_inv [where P="cte_at' p0" for p0]
                       checkCap_inv [where P="valid_cap' c" for c]
                       checkCap_inv [where P="sch_act_simple"]
                          | simp)+
            apply (simp add: guard_is_UNIV_def)
           apply (thin_tac "ccorres a1 a2 a3 a4 a5 a6 a7" for a1 a2 a3 a4 a5 a6 a7)
           apply (rule ccorres_rhs_assoc)+
           apply (rule checkCapAt_ccorres2)
              apply ceqv
             apply csymbr
             apply (simp add: if_1_0_0 true_def Collect_True
                         del: Collect_const)
             apply (rule ccorres_rhs_assoc)+
             apply (rule checkCapAt_ccorres2)
                apply ceqv
               apply csymbr
               apply (simp add: if_1_0_0 true_def Collect_True
                                assertDerived_def bind_assoc
                                ccorres_cond_iffs dc_def[symmetric]
                           del: Collect_const)
               apply (rule ccorres_symb_exec_l)
                  apply (ctac add: cteInsert_ccorres)
                 apply (wp empty_fail_stateAssert
                           hoare_case_option_wp | simp del: Collect_const)+
              apply csymbr
              apply (simp add: if_1_0_0 false_def Collect_False ccorres_cond_iffs
                          del: Collect_const)
              apply (rule ccorres_return_Skip[unfolded dc_def])
             apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem
                                   tcbVTable_def tcbVTableSlot_def
                                   cte_level_bits_def size_of_def option_to_0_def)
            apply csymbr
            apply (simp add: if_1_0_0 false_def Collect_False
                        del: Collect_const)
            apply (rule ccorres_cond_false)
            apply (rule ccorres_return_Skip[unfolded dc_def])
           apply (clarsimp simp: guard_is_UNIV_def false_def
                                 ccap_relation_def cap_thread_cap_lift
                                 cap_to_H_def)
          apply simp
          apply (rule ccorres_split_throws, rule ccorres_return_C_errorE, simp+)
          apply vcg
         apply (simp add: conj_comms, simp cong: conj_cong add: invs_mdb' invs_pspace_aligned')
         apply (simp add: cte_is_derived_capMasterCap_strg o_def)
         apply (wp cteDelete_invs' hoare_case_option_wp cteDelete_deletes
                   cteDelete_sch_act_simple
                | strengthen impI[OF invs_valid_objs'])+
         apply (rule hoare_post_imp_R[where Q' = "\<lambda>r. invs'"])
          apply (wp cteDelete_invs')
         apply (clarsimp simp:cte_wp_at_ctes_of)
        apply simp
       apply (rule ccorres_Cond_rhs_Seq)
        apply (rule ccorres_rhs_assoc)+
        apply csymbr
        apply (rule ccorres_Guard_Seq)+
        apply (simp add: split_def getThreadCSpaceRoot_def locateSlot_conv
                         bindE_assoc
                    del: Collect_const)
        apply csymbr
        apply (ctac(no_vcg) add: cteDelete_ccorres)
          apply (simp add: liftE_bindE Collect_False ccorres_cond_iffs
                           dc_def
                      del: Collect_const)
          apply ((rule ccorres_split_nothrow_novcg_dc[rotated], assumption)
                  | rule ccorres_rhs_assoc2)+
            apply (simp add: conj_comms pred_conj_def)
            apply (simp add: o_def cong: conj_cong option.case_cong)
            apply (wp checked_insert_tcb_invs' hoare_case_option_wp
                      checkCap_inv [where P="tcb_at' p0" for p0]
                      checkCap_inv [where P="cte_at' p0" for p0]
                      checkCap_inv [where P="valid_cap' c" for c]
                      checkCap_inv [where P="sch_act_simple"]
                         | simp)+
           apply (clarsimp simp: guard_is_UNIV_def from_bool_def true_def
                                 word_sle_def if_1_0_0 Collect_const_mem
                                 option_to_0_def Kernel_C.tcbVTable_def tcbVTableSlot_def
                                 cte_level_bits_def size_of_def cintr_def)
          apply (thin_tac "ccorres a1 a2 a3 a4 a5 a6 a7" for a1 a2 a3 a4 a5 a6 a7)
          apply (rule ccorres_rhs_assoc)+
          apply (rule checkCapAt_ccorres2)
             apply ceqv
            apply csymbr
            apply (simp add: if_1_0_0 true_def Collect_True
                        del: Collect_const)
            apply (rule ccorres_rhs_assoc)+
            apply (rule checkCapAt_ccorres2)
               apply ceqv
              apply csymbr
              apply (simp add: if_1_0_0 true_def Collect_True
                               assertDerived_def bind_assoc
                               ccorres_cond_iffs dc_def[symmetric]
                          del: Collect_const)
              apply (rule ccorres_symb_exec_l)
                 apply (ctac add: cteInsert_ccorres)
                apply (wp empty_fail_stateAssert
                          hoare_case_option_wp | simp del: Collect_const)+
             apply csymbr
             apply (simp add: if_1_0_0 false_def Collect_False ccorres_cond_iffs
                         del: Collect_const)
             apply (rule ccorres_return_Skip[unfolded dc_def])
            apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem
                                  Kernel_C.tcbCTable_def tcbCTableSlot_def
                                  cte_level_bits_def size_of_def option_to_0_def)
           apply csymbr
           apply (simp add: if_1_0_0 false_def Collect_False
                       del: Collect_const)
           apply (rule ccorres_cond_false)
           apply (rule ccorres_return_Skip[unfolded dc_def])
          apply (clarsimp simp: guard_is_UNIV_def false_def
                                ccap_relation_def cap_thread_cap_lift
                                cap_to_H_def)
         apply simp
         apply (rule ccorres_split_throws, rule ccorres_return_C_errorE, simp+)
         apply vcg
        apply (simp add: conj_comms, simp cong: conj_cong add: invs_mdb' invs_pspace_aligned')
        apply (simp add: cte_is_derived_capMasterCap_strg o_def)
        apply (wp cteDelete_invs' hoare_case_option_wp cteDelete_deletes
                  cteDelete_sch_act_simple 
               | strengthen impI[OF invs_valid_objs'])+
        apply (rule hoare_post_imp_R[where Q' = "\<lambda>r. invs'"])
         apply (wp cteDelete_invs')
        apply (clarsimp simp:cte_wp_at_ctes_of)
       apply simp
      apply (wp hoare_case_option_wp setP_invs' static_imp_wp | simp)+
     apply (clarsimp simp: guard_is_UNIV_def tcbCTableSlot_def Kernel_C.tcbCTable_def
                           cte_level_bits_def size_of_def word_sle_def option_to_0_def
                           true_def from_bool_def cintr_def)
    apply (simp add: conj_comms)
    apply (wp hoare_case_option_wp threadSet_invs_trivial
              threadSet_cap_to' static_imp_wp | simp)+
   apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem)
  apply (clarsimp simp: inQ_def)
  apply (subst is_aligned_neg_mask [OF _ order_refl])
   apply (simp add: tcb_ptr_to_ctcb_ptr_def)
   apply (rule aligned_add_aligned)
      apply (fastforce simp add: obj_at'_def projectKOs objBits_simps)
     apply (simp add: ctcb_offset_def is_aligned_def)
    apply (simp add: word_bits_conv)
   apply simp
  apply (subgoal_tac "s \<turnstile>' capability.ThreadCap target")
   apply (clarsimp simp: cte_level_bits_def Kernel_C.tcbCTable_def Kernel_C.tcbVTable_def
                         tcbCTableSlot_def tcbVTableSlot_def size_of_def
                         tcb_cte_cases_def isCap_simps
                  split: option.split_asm
                  dest!: isValidVTableRootD)
  apply (clarsimp simp: valid_cap'_def capAligned_def  word_bits_conv
                        obj_at'_def objBits_simps projectKOs)
  done

lemma setupReplyMaster_ccorres:
  "ccorres dc xfdc (tcb_at' t)
        (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr t}) []
        (setupReplyMaster t) (Call setupReplyMaster_'proc)"
  apply (cinit lift: thread_')
   apply (rule ccorres_Guard_Seq)+
   apply ctac
     apply (simp del: Collect_const add: dc_def[symmetric])
     apply (rule ccorres_pre_getCTE)
     apply (rule ccorres_move_c_guard_cte)
     apply (rule_tac F="\<lambda>rv'. (rv' = scast cap_null_cap) = (cteCap oldCTE = NullCap)"
                 and R="cte_wp_at' (op = oldCTE) rv"
               and xf'=ret__unsigned_long_'
                  in ccorres_symb_exec_r_abstract_UNIV[where R'=UNIV])
        apply (rule conseqPre, vcg)
        apply (clarsimp simp: cte_wp_at_ctes_of)
        apply (erule(1) cmap_relationE1[OF cmap_relation_cte])
        apply (clarsimp simp: typ_heap_simps cap_get_tag_isCap
                       dest!: ccte_relation_ccap_relation)
       apply ceqv
      apply (simp only:)
      apply (rule ccorres_when[where R=\<top>])
       apply (simp add: Collect_const_mem)
      apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_stateAssert])
        apply (rule_tac P="cte_at' rv and tcb_at' t" in ccorres_from_vcg[where P'=UNIV])
        apply (rule allI, rule conseqPre, vcg)
        apply (clarsimp simp: cte_wp_at_ctes_of)
        apply (rule cmap_relationE1[OF cmap_relation_cte], assumption+)
        apply (rule conjI, fastforce intro: typ_heap_simps)
        apply (clarsimp simp: typ_heap_simps)
        apply (rule fst_setCTE[OF ctes_of_cte_at], assumption)
        apply (rule rev_bexI, assumption)
        apply (clarsimp simp: rf_sr_def cstate_relation_def
                              cpspace_relation_def Let_def)
        apply (subst setCTE_tcb_case, assumption+)
        apply (rule_tac r="s'" in KernelStateData_H.kernel_state.cases)
        apply clarsimp
        apply (rule conjI)
         apply (erule(2) cmap_relation_updI)
          apply (clarsimp simp: ccte_relation_def cap_reply_cap_lift
                                cte_lift_def)
          apply (simp add: cte_to_H_def cap_to_H_def mdb_node_to_H_def
                           nullMDBNode_def c_valid_cte_def)
          apply (simp add: cap_reply_cap_lift)
          apply (subst is_aligned_neg_mask)
            apply (erule is_aligned_tcb_ptr_to_ctcb_ptr)
           apply simp
          apply (simp add: true_def mask_def to_bool_def)
         apply simp
        apply (simp add: cmachine_state_relation_def 
                         h_t_valid_clift_Some_iff
                         carch_state_relation_def carch_globals_def)
       apply (wp | simp)+
     apply (clarsimp simp: guard_is_UNIV_def)
    apply (wp | simp add: locateSlot_conv)+
   apply vcg
  apply (clarsimp simp: word_sle_def cte_wp_at_ctes_of
                        tcbReplySlot_def tcbReply_def)
  done

lemma restart_ccorres:
  "ccorres dc xfdc (invs' and tcb_at' thread and sch_act_simple)
        (UNIV \<inter> {s. target_' s = tcb_ptr_to_ctcb_ptr thread}) []
     (restart thread) (Call restart_'proc)"
  apply (cinit lift: target_')
   apply (ctac(no_vcg) add: isBlocked_ccorres)
    apply (simp only: when_def)
    apply (rule ccorres_cond2[where R=\<top>])
      apply (simp add: to_bool_def Collect_const_mem)
     apply (rule ccorres_rhs_assoc)+
     apply (ctac(no_vcg) add: ipcCancel_ccorres1[OF cteDeleteOne_ccorres])
      apply (ctac(no_vcg) add: setupReplyMaster_ccorres)
       apply (ctac(no_vcg))
        apply (ctac(no_vcg) add: tcbSchedEnqueue_ccorres)
         apply ctac
        apply (wp weak_sch_act_wf_lift)[1]
       apply (wp sts_valid_queues setThreadState_st_tcb)[1]
      apply (simp add: valid_tcb_state'_def)
      apply wp
      apply (wp_once sch_act_wf_lift, wp tcb_in_cur_domain'_lift)
     apply (rule hoare_strengthen_post)
      apply (rule hoare_vcg_conj_lift)
       apply (rule delete_one_conc_fr.ipcCancel_invs)
      apply (rule ipcCancel_tcb'[where t=thread])
     apply fastforce
    apply (rule ccorres_return_Skip)
   apply (wp hoare_drop_imps)
  apply (auto simp: Collect_const_mem mask_def "StrictC'_thread_state_defs")
  done

lemma setNextPC_ccorres:
  "ccorres dc xfdc \<top>
       (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>
             \<inter> {s. v_' s = val}) []
       (asUser thread (setNextPC val))
       (Call setNextPC_'proc)"
  apply (cinit')
   apply (simp add: setNextPC_def)
   apply (ctac add: setRegister_ccorres)
  apply simp
  done

lemma Arch_performTransfer_ccorres:
  "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
            \<top> UNIV []
       (liftE (performTransfer a b c))
       (Call Arch_performTransfer_'proc)"
  apply (cinit' simp: performTransfer_def)
   apply (fold returnOk_liftE)
   apply (rule ccorres_return_CE)
     apply simp+
  done

lemma frame_gp_registers_convs:
  "length State_H.frameRegisters = unat n_frameRegisters"
  "length State_H.gpRegisters = unat n_gpRegisters"
  "n < length State_H.frameRegisters \<Longrightarrow>
     index frameRegisters n = register_from_H (State_H.frameRegisters ! n)"
  "n < length State_H.gpRegisters \<Longrightarrow>
     index gpRegisters n = register_from_H (State_H.gpRegisters ! n)"
  apply (simp_all add: State_H.gpRegisters_def State_H.frameRegisters_def
                       ARMMachineTypes.gpRegisters_def n_gpRegisters_def
                       ARMMachineTypes.frameRegisters_def n_frameRegisters_def
                       frameRegisters_def gpRegisters_def msgRegisters_unfold
                       fupdate_def Arrays.update_def toEnum_def
                       upto_enum_def fromEnum_def enum_register)
  apply (auto simp: less_Suc_eq fcp_beta Kernel_C.LR_def R14_def)
  done

lemma invokeTCB_CopyRegisters_ccorres:
  "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_')
   (invs' and sch_act_simple and tcb_at' destn and tcb_at' source
          and ex_nonz_cap_to' destn and ex_nonz_cap_to' source)
   (UNIV \<inter> {s. dest_' s = tcb_ptr_to_ctcb_ptr destn}
         \<inter> {s. tcb_src_' s = tcb_ptr_to_ctcb_ptr source}
         \<inter> {s. to_bool (resumeTarget_' s) = resume}
         \<inter> {s. to_bool (suspendSource_' s) = susp}
         \<inter> {s. to_bool (transferFrame_' s) = frames}
         \<inter> {s. to_bool (transferInteger_' s) = ints}) []
   (invokeTCB (CopyRegisters destn source susp resume frames ints arch))
   (Call invokeTCB_CopyRegisters_'proc)"
  apply (cinit lift: dest_' tcb_src_' resumeTarget_'
                     suspendSource_' transferFrame_' transferInteger_'
               simp: whileAnno_def)
   apply (simp add: liftE_def bind_assoc whileAnno_def
               del: Collect_const)
   apply (rule ccorres_split_nothrow_novcg_dc)
      apply (rule ccorres_when[where R=\<top>])
       apply (simp add: to_bool_def del: Collect_const)
      apply (ctac add: suspend_ccorres[OF cteDeleteOne_ccorres])
     apply (rule ccorres_split_nothrow_novcg_dc)
        apply (rule ccorres_when[where R=\<top>])
         apply (simp add: to_bool_def del: Collect_const)
        apply (ctac add: restart_ccorres)
       apply (rule ccorres_split_nothrow_novcg_dc)
          apply (rule ccorres_when[where R=\<top>])
           apply (simp add: to_bool_def Collect_const_mem)
          apply (rule ccorres_rhs_assoc)+
          apply (csymbr, csymbr, csymbr)
          apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg_dc)
             apply (rule ccorres_rel_imp)
              apply (rule ccorres_mapM_x_while[where F="\<lambda>x. tcb_at' destn and tcb_at' source"])
                  apply clarsimp
                  apply (rule ccorres_guard_imp2)
                   apply (ctac(no_vcg) add: getRegister_ccorres)
                    apply (ctac add: setRegister_ccorres)
                   apply wp
                  apply (clarsimp simp: frame_gp_registers_convs
                                        n_frameRegisters_def unat_of_nat32
                                        word_bits_def word_of_nat_less)
                 apply (simp add: frame_gp_registers_convs n_frameRegisters_def)
                apply (rule allI, rule conseqPre, vcg)
                apply clarsimp
               apply (wp | simp)+
              apply (simp add: frame_gp_registers_convs n_frameRegisters_def
                               word_bits_def)
             apply simp
            apply (ctac(no_vcg) add: getRestartPC_ccorres)
             apply (ctac add: setNextPC_ccorres)
            apply wp
          apply (clarsimp simp: guard_is_UNIV_def)
         apply (rule ccorres_split_nothrow_novcg_dc)
            apply (rule ccorres_when[where R=\<top>])
             apply (simp add: to_bool_def Collect_const_mem)
            apply (rule ccorres_rhs_assoc)+
            apply (csymbr, csymbr)
            apply (rule ccorres_rel_imp)
             apply (rule ccorres_mapM_x_while[where F="\<lambda>x. tcb_at' destn and tcb_at' source"])
                 apply clarsimp
                 apply (rule ccorres_guard_imp2)
                  apply ((wp | ctac(no_vcg) add: getRegister_ccorres setRegister_ccorres)+)[1]
                 apply (clarsimp simp: frame_gp_registers_convs n_gpRegisters_def
                                       unat_of_nat32 word_bits_def word_of_nat_less)
                apply (simp add: frame_gp_registers_convs n_gpRegisters_def)
               apply (rule allI, rule conseqPre, vcg)
               apply clarsimp
              apply (wp | simp)+
             apply (simp add: word_bits_def frame_gp_registers_convs n_gpRegisters_def)
            apply simp
           apply (simp only: liftE_bindE[symmetric] return_returnOk)
           apply (ctac(no_vcg) add: Arch_performTransfer_ccorres)
             apply (rule ccorres_return_CE, simp+)[1]
            apply (rule ccorres_return_C_errorE, simp+)[1]
           apply wp
         apply (simp add: pred_conj_def guard_is_UNIV_def cong: if_cong
                   | wp mapM_x_wp' static_imp_wp)+
  apply (clarsimp simp: Collect_const_mem from_bool_def true_def split: split_if)
  apply (auto simp: invs'_def valid_state'_def global'_no_ex_cap)
  done

(* FIXME: move *)
lemma mapM_x_append:
  "mapM_x f (xs @ ys) = do mapM_x f xs; mapM_x f ys od"
  apply (simp add: mapM_x_def sequence_x_def)
  apply (induct xs)
   apply simp
  apply (simp add: bind_assoc)
  done

lemma invokeTCB_WriteRegisters_ccorres_helper:
  "\<lbrakk> unat (f (of_nat n)) = incn
         \<and> g (of_nat n) = register_from_H reg \<and> n'=incn
         \<and> of_nat n < bound \<and> of_nat n < bound2 \<rbrakk> \<Longrightarrow>
   ccorres dc xfdc (sysargs_rel args buffer and sysargs_rel_n args buffer n' and P) \<lbrace>\<acute>i = of_nat n\<rbrace> hs
     (asUser dst (setRegister reg
          (sanitiseRegister reg (args ! incn))))
     (\<acute>ret__unsigned_long :== CALL getSyscallArg(f (\<acute>i),option_to_ptr buffer);;
      Guard ArrayBounds \<lbrace>\<acute>i < bound\<rbrace>
        (\<acute>unsigned_long_eret_2 :== CALL sanitiseRegister(g (\<acute>i),\<acute>ret__unsigned_long));;
      Guard ArrayBounds \<lbrace>\<acute>i < bound2\<rbrace>
        (CALL setRegister(tcb_ptr_to_ctcb_ptr dst,g (\<acute>i),\<acute>unsigned_long_eret_2)))"
  apply (rule ccorres_guard_imp2)
   apply (rule ccorres_add_return)
   apply (rule ccorres_rhs_assoc)+ 
   apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n="incn" and buffer=buffer])
     apply (rule ccorres_symb_exec_r)
       apply (ctac add: setRegister_ccorres)
      apply vcg
     apply (rule conseqPre, vcg, clarsimp)
    apply wp
   apply simp
   apply (vcg exspec=getSyscallArg_modifies)
  apply clarsimp
  done

lemma doMachineOp_context:
  "(rv,s') \<in> fst (doMachineOp f s) \<Longrightarrow>
  (rv,s'\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)
  \<in> fst (doMachineOp f (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>))"
  apply (clarsimp simp: doMachineOp_def split_def in_monad select_f_def)
  apply fastforce
  done


lemma getObject_context:
  " \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk>
  \<Longrightarrow> (if t = t' then tcbContext_update (\<lambda>_. st) x else x, 
      s'\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)
      \<in> fst (getObject t' (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>))"
  apply (simp split: split_if)
  apply (rule conjI)
   apply clarsimp
   apply (clarsimp simp: getObject_def split_def loadObject_default_def in_monad 
                         Corres_C.in_magnitude_check' projectKOs objBits_simps)
   apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs objBits_simps)
   apply (simp add: magnitudeCheck_def in_monad split: option.splits)
   apply clarsimp
   apply (simp add: lookupAround2_char2)
   apply (clarsimp split: split_if_asm)
   apply (erule_tac x=x2 in allE)
   apply (clarsimp simp: ps_clear_def)
   apply (drule_tac x=x2 in orthD2)
    apply fastforce
   apply clarsimp
   apply (erule impE)
    apply simp
   apply (erule notE, rule word_diff_ls'(3))
    apply unat_arith
   apply (drule is_aligned_no_overflow)
   apply simp
  apply clarsimp
  apply (clarsimp simp: getObject_def split_def loadObject_default_def in_monad 
                        Corres_C.in_magnitude_check' projectKOs objBits_simps)
  apply (simp add: magnitudeCheck_def in_monad split: option.splits)
  apply clarsimp
  apply (simp add: lookupAround2_char2)
  apply (clarsimp split: split_if_asm)
   apply (erule_tac x=t in allE)
   apply simp
   apply (clarsimp simp: obj_at'_real_def projectKOs 
                         ko_wp_at'_def objBits_simps)
   apply (simp add: ps_clear_def)
   apply (drule_tac x=t in orthD2)
    apply fastforce
   apply clarsimp
   apply (erule impE)
    apply simp
   apply (erule notE, rule word_diff_ls'(3))
    apply unat_arith
   apply (drule is_aligned_no_overflow)
   apply simp  
  apply (erule_tac x=x2 in allE)
  apply (clarsimp simp: ps_clear_def)
  apply (drule_tac x=x2 in orthD2)
   apply fastforce
  apply clarsimp
  apply (erule impE)
   apply (rule word_diff_ls'(3))
   apply unat_arith
   apply (drule is_aligned_no_overflow)
   apply simp
  apply fastforce
  done

lemma threadGet_context:
  "\<lbrakk> (uc, s') \<in> fst (threadGet tcbContext (ksCurThread s) s); ko_at' ko t s;
      t \<noteq> ksCurThread s \<rbrakk> \<Longrightarrow>
   (uc, s'\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> 
  fst (threadGet tcbContext (ksCurThread s) (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>))"
  apply (clarsimp simp: threadGet_def liftM_def in_monad) 
  apply (drule (1) getObject_context [where st=st])   
  apply (rule exI)
  apply (erule conjI)
  apply (simp split: if_splits) 
done


lemma asUser_context:
  "\<lbrakk>(x,s) \<in> fst (asUser (ksCurThread s) f s); ko_at' ko t s; \<And>s. \<lbrace>op = s\<rbrace> f \<lbrace>\<lambda>_. op = s\<rbrace> ; 
    t \<noteq> ksCurThread s\<rbrakk> \<Longrightarrow>
  (x,s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> 
  fst (asUser (ksCurThread s) f (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>))"
  apply (clarsimp simp: asUser_def in_monad select_f_def)
  apply (frule use_valid, rule threadGet_inv [where P="op = s"], rule refl)
  apply (frule use_valid, assumption, rule refl)
  apply clarsimp
  apply (frule (2) threadGet_context)
  apply (intro exI)
  apply (erule conjI)
  apply (rule exI, erule conjI)
  apply (clarsimp simp: threadSet_def in_monad)
  apply (frule use_valid, rule getObject_inv [where P="op = s"])
    apply (simp add: loadObject_default_def)
    apply wp
    apply simp
   apply (rule refl)
  apply clarsimp
  apply (frule (1) getObject_context)
  apply (intro exI)
  apply (erule conjI)
  apply (clarsimp simp: setObject_def split_def updateObject_default_def threadGet_def
                        Corres_C.in_magnitude_check' getObject_def loadObject_default_def liftM_def
                        objBits_simps projectKOs in_monad)

  apply (clarsimp simp: magnitudeCheck_def in_monad split: option.splits)
  apply (rule conjI)
   apply clarsimp
   apply (cases s, simp)
   apply (rule ext, clarsimp split: split_if) 
   apply (case_tac tcb, simp)

  apply clarsimp
  apply (rule conjI)
   apply (clarsimp simp add: lookupAround2_char2 split: split_if_asm)
    apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs objBits_simps)
    apply (erule_tac x=t in allE)
    apply simp
    apply (simp add: ps_clear_def)
    apply (drule_tac x=t in orthD2)
     apply fastforce
    apply clarsimp
    apply (erule impE, simp)
    apply (erule notE, rule word_diff_ls'(3))
     apply unat_arith
    apply (drule is_aligned_no_overflow)
    apply simp
   apply (erule_tac x=x2 in allE)
   apply simp
   apply (simp add: ps_clear_def)
   apply (drule_tac x=x2 in orthD2)
    apply fastforce
   apply clarsimp
   apply (erule impE)
    apply (rule word_diff_ls'(3))
     apply unat_arith
    apply (drule is_aligned_no_overflow)
    apply simp
   apply (erule impE, simp)
   apply simp
  apply (rule exI)
  apply (rule conjI, fastforce)
  apply clarsimp
  apply (cases s, clarsimp)
  apply (rule ext, clarsimp split: split_if)
  apply (case_tac tcb, clarsimp)
done


lemma getMRs_rel_context:
  "\<lbrakk>getMRs_rel args buffer s; 
    (cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer) s;
    ko_at' ko t s ; t \<noteq> ksCurThread s\<rbrakk> \<Longrightarrow>
  getMRs_rel args buffer (s\<lparr>ksPSpace := ksPSpace s(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)"
  apply (clarsimp simp: getMRs_rel_def)
  apply (rule exI, erule conjI)
  apply (subst (asm) det_wp_use, rule det_wp_getMRs)
   apply (simp add: cur_tcb'_def)
  apply (subst det_wp_use, rule det_wp_getMRs)
   apply (simp add: cur_tcb'_def)
   apply (rule conjI)
    apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs 
                          objBits_simps ps_clear_def split: split_if)
   apply (clarsimp simp: valid_ipc_buffer_ptr'_def split: option.splits)
   apply (clarsimp simp: typ_at'_def ko_wp_at'_def projectKOs obj_at'_real_def
                         objBits_simps ps_clear_def split: split_if)
  apply (clarsimp simp: getMRs_def in_monad)
  apply (frule use_valid, rule asUser_inv [where P="op = s"])
    apply (wp mapM_wp' getRegister_inv)[1]
   apply simp
  apply clarsimp
  apply (drule (1) asUser_context)
    apply (wp mapM_wp' getRegister_inv)[1] 
   apply assumption
  apply (intro exI)
  apply (erule conjI)
  apply (cases buffer)
   apply (clarsimp simp: return_def)
  apply clarsimp 
  apply (drule mapM_upd_inv [rotated -1]) 
    prefer 3
    apply fastforce
   prefer 2
   apply wp
  apply (clarsimp simp: loadWordUser_def in_monad stateAssert_def word_size
                  simp del: fun_upd_apply)
  apply (rule conjI)
   apply (clarsimp simp: pointerInUserData_def typ_at'_def ko_wp_at'_def 
                         projectKOs ps_clear_def obj_at'_real_def
                  split: split_if)
  apply (erule doMachineOp_context)
done

lemma asUser_getMRs_rel:
  "\<lbrace>(\<lambda>s. t \<noteq> ksCurThread s) and getMRs_rel args buffer and cur_tcb' 
        and case_option \<top> valid_ipc_buffer_ptr' buffer \<rbrace> 
  asUser t f \<lbrace>\<lambda>_. getMRs_rel args buffer\<rbrace>"
  apply (simp add: asUser_def)
  apply (rule hoare_pre, wp)
     apply (simp add: threadSet_def)
     apply (simp add: setObject_def split_def updateObject_default_def)
     apply wp
     apply (simp del: fun_upd_apply)
     apply (wp getObject_tcb_wp)
   apply (wp threadGet_wp)
  apply (clarsimp simp del: fun_upd_apply)
  apply (drule obj_at_ko_at')+
  apply (clarsimp simp del: fun_upd_apply)
  apply (rule exI, rule conjI, assumption)
  apply (clarsimp split: split_if simp del: fun_upd_apply)
  apply (erule getMRs_rel_context, simp)
   apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs)
  apply simp
done


lemma asUser_sysargs_rel:
  "\<lbrace>\<lambda>s. t \<noteq> ksCurThread s \<and> sysargs_rel args buffer s\<rbrace> 
  asUser t f \<lbrace>\<lambda>_. sysargs_rel args buffer\<rbrace>"
  apply (cases buffer, simp_all add: sysargs_rel_def)
   apply (rule hoare_pre)
   apply (wp asUser_getMRs_rel hoare_valid_ipc_buffer_ptr_typ_at'|simp)+
done


lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]:
  notes static_imp_wp [wp]
  shows
  "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_')
   (invs' and tcb_at' dst and ex_nonz_cap_to' dst and sch_act_simple
          and sysargs_rel args buffer
          and (\<lambda>s. dst \<noteq> ksCurThread s)
          and (\<lambda>_. values = take someNum (drop 2 args)
                   \<and> someNum + 2 \<le> length args))
   ({s. unat (n_' s) = length values} \<inter> S
         \<inter> {s. unat (n_' s) = length values}
         \<inter> {s. dest_' s = tcb_ptr_to_ctcb_ptr dst}
         \<inter> {s. resumeTarget_' s = from_bool resume}
         \<inter> {s. buffer_' s = option_to_ptr buffer}) []
   (invokeTCB (WriteRegisters dst resume values arch))
   (Call invokeTCB_WriteRegisters_'proc)"
  apply (rule ccorres_gen_asm)
  apply (erule conjE)
  apply (cinit lift: n_' dest_' resumeTarget_' buffer_'
               simp: whileAnno_def)
   (* using S not univ seems to stop cinit doing this? *)
   apply (csymbr, csymbr, csymbr)
   apply (simp add: liftE_def bind_assoc
               del: Collect_const)
   apply (rule ccorres_pre_getCurThread)
   apply (rule_tac P="\<lambda>a. ccorres_underlying rf_sr \<Gamma> r' xf arrel axf P P' hs a c" for r' xf arrel axf P P' hs c in subst)
    apply (rule liftE_bindE)

   apply (ctac add: Arch_performTransfer_ccorres)
      apply (simp add: Collect_False whileAnno_def del: Collect_const)
      apply (rule ccorres_add_return)
      apply (rule_tac xf'=n_' and r'="\<lambda>rv rv'. rv' = min n (scast n_frameRegisters + scast n_gpRegisters)"
                    in ccorres_split_nothrow)
          apply (rule_tac P'="{s. n_' s = n}" in ccorres_from_vcg[where P=\<top>])
          apply (rule allI, rule conseqPre, vcg)
          apply (clarsimp simp: return_def min_def)
          apply (simp add: linorder_not_less[symmetric]
                           n_gpRegisters_def n_frameRegisters_def)
         apply ceqv
        apply (simp add: zipWithM_mapM split_def zip_append1
                         mapM_discarded mapM_x_append
                    del: Collect_const)
        apply (simp add: asUser_bind_distrib getRestartPC_def setNextPC_def
                         bind_assoc del: Collect_const)
        apply (simp only: getRestartPC_def[symmetric] setNextPC_def[symmetric])
        apply (simp add: asUser_mapM_x bind_assoc)
        apply (rule ccorres_stateAssert)
        apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg) 
            apply (rule_tac F="\<lambda>n. sysargs_rel args buffer and sysargs_rel_n args buffer (n + 2)
                                     and (\<lambda>s. dst \<noteq> ksCurThread s)"
                        and Q=UNIV
                         in ccorres_mapM_x_whileQ)
                 apply clarsimp
                 apply (rule_tac invokeTCB_WriteRegisters_ccorres_helper
                                       [where args=args])
                 apply (simp add: unat_word_ariths frame_gp_registers_convs
                                  n_frameRegisters_def unat_of_nat32 word_bits_def
                                  word_of_nat_less)
                apply (simp add: n_frameRegisters_def n_gpRegisters_def
                                 frame_gp_registers_convs word_less_nat_alt)
                apply (simp add: unat_of_nat32 word_bits_def)
                apply arith
               apply (vcg exspec=setRegister_modifies exspec=getSyscallArg_modifies
                          exspec=sanitiseRegister_modifies)
               apply clarsimp
              apply (simp add: sysargs_rel_n_def)
              apply (rule hoare_pre, wp asUser_sysargs_rel)
              apply (clarsimp simp: n_msgRegisters_def sysargs_rel_def)
             apply (simp add: frame_gp_registers_convs n_frameRegisters_def
                              word_bits_def)
            apply simp
           apply (rule ceqv_refl)
          apply (rule ccorres_stateAssert)
          apply (rule ccorres_rhs_assoc2, rule ccorres_split_nothrow_novcg) 
              apply (rule_tac F="\<lambda>n. sysargs_rel args buffer 
                                     and sysargs_rel_n args buffer (n + length State_H.frameRegisters + 2)
                                     and (\<lambda>s. dst \<noteq> ksCurThread s)"
                          and Q=UNIV
                           in ccorres_mapM_x_whileQ)
                   apply clarsimp
                   apply (rule invokeTCB_WriteRegisters_ccorres_helper
                                       [where args=args])
                   apply (simp add: n_gpRegisters_def unat_word_ariths
                                    frame_gp_registers_convs unat_of_nat32
                                    word_bits_def n_frameRegisters_def
                                    word_of_nat_less)
                  apply (simp add: n_frameRegisters_def n_gpRegisters_def
                                   frame_gp_registers_convs unat_of_nat32
                                   word_less_nat_alt word_bits_def
                                   less_diff_conv)
                  apply (simp add: unat_word_ariths cong: conj_cong)
                 apply (vcg exspec=setRegister_modifies exspec=getSyscallArg_modifies
                            exspec=sanitiseRegister_modifies)
                 apply clarsimp
                apply (simp add: sysargs_rel_n_def)
                apply (rule hoare_pre, wp asUser_sysargs_rel)
                apply (clarsimp simp: n_msgRegisters_def frame_gp_registers_convs
                                      n_frameRegisters_def)
                apply arith
               apply (simp add: State_H.gpRegisters_def word_bits_def
                                ARMMachineTypes.gpRegisters_def)
              apply simp
             apply (rule ceqv_refl)
            apply (ctac(no_vcg) add: getRestartPC_ccorres)
             apply simp
             apply (ctac(no_vcg) add: setNextPC_ccorres)
              apply (rule ccorres_split_nothrow_novcg)
                  apply (rule ccorres_when[where R=\<top>])
                   apply (simp add: from_bool_0 Collect_const_mem)
                  apply (rule_tac xf'="\<lambda>_. 0" in ccorres_call)
                     apply (rule restart_ccorres)
                    apply simp
                   apply (simp add: xfdc_def)
                  apply simp
                 apply (rule ceqv_refl)
                apply (unfold return_returnOk)[1]
                apply (rule ccorres_return_CE, simp+)[1]
               apply wp
              apply (simp add: guard_is_UNIV_def)
             apply wp
             apply (simp del: hoare_post_taut)
            apply (rule mapM_x_wp')
            apply (rule hoare_pre, wp)
            apply clarsimp
           apply (simp del: hoare_post_taut)
           apply wp
          apply (simp add: guard_is_UNIV_def)
         apply (rule hoare_drop_imps)
         apply (simp add: sysargs_rel_n_def)
         apply (wp mapM_x_wp')
          apply (rule hoare_pre, wp asUser_sysargs_rel)
          apply clarsimp
         apply (rule hoare_pre, wp)
         apply simp
        apply (simp add: guard_is_UNIV_def)
       apply (wp)
      apply vcg
     apply (rule ccorres_inst[where P=\<top> and P'=UNIV])
     apply simp
    apply (simp add: performTransfer_def)
    apply wp
   apply vcg
  apply (clarsimp simp: n_msgRegisters_def sysargs_rel_n_def split: split_if)
  apply (rule conjI)
   apply (cases args, simp)
   apply (case_tac list, simp)
   apply (case_tac lista, clarsimp simp: unat_eq_0)
   apply simp
  apply (clarsimp simp: frame_gp_registers_convs word_less_nat_alt
                        sysargs_rel_def n_frameRegisters_def n_msgRegisters_def
                 split: split_if_asm)
  done 

lemma invokeTCB_Suspend_ccorres:
  "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_')
     (invs' and sch_act_simple and tcb_at' t and ex_nonz_cap_to' t)
     (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr t}) []
   (invokeTCB (Suspend t)) (Call invokeTCB_Suspend_'proc)"
  apply (cinit lift: thread_')
   apply (simp add: liftE_def return_returnOk)
   apply (ctac(no_vcg) add: suspend_ccorres[OF cteDeleteOne_ccorres])
    apply (rule ccorres_return_CE, simp+)[1]
   apply wp
  apply (clarsimp simp: from_bool_def true_def)
  apply (auto simp: invs'_def valid_state'_def global'_no_ex_cap)
  done

lemma invokeTCB_Resume_ccorres:
  "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_')
     (invs' and tcb_at' t and ex_nonz_cap_to' t and sch_act_simple)
     (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr t}) []
   (invokeTCB (Resume t)) (Call invokeTCB_Resume_'proc)"
  apply (cinit lift: thread_')
   apply (simp add: liftE_def return_returnOk)
   apply (ctac(no_vcg) add: restart_ccorres)
    apply (rule ccorres_return_CE, simp+)[1]
   apply wp
  apply (clarsimp simp: from_bool_def true_def)
  done

lemma Arch_decodeTransfer_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s} Call Arch_decodeTransfer_'proc {s'. ret__unsigned_long_' s' = 0}"
  by (vcg, simp)

lemmas ccorres_split_nothrow_dc
    = ccorres_split_nothrow[where r'=dc and xf'=xfdc, OF _ ceqv_refl]

lemmas getRegister_ccorres_defer
    = ccorres_defer[OF getRegister_ccorres, OF no_fail_asUser [OF no_fail_getRegister]]

lemma msg_registers_convs:
  "length State_H.msgRegisters = unat n_msgRegisters"
  "n < length State_H.msgRegisters \<Longrightarrow>
     index msgRegisters n = register_from_H (State_H.msgRegisters ! n)"
  apply (simp_all add: msgRegisters_unfold
                       ARMMachineTypes.msgRegisters_def n_msgRegisters_def
                       msgRegisters_def fupdate_def Arrays.update_def)
  apply (auto simp: less_Suc_eq fcp_beta)
  done

lemma mapM_x_split_append:
  "mapM_x f xs = do _ \<leftarrow> mapM_x f (take n xs); mapM_x f (drop n xs) od"
  using mapM_x_append[where f=f and xs="take n xs" and ys="drop n xs"]
  by simp

lemma ccorres_abstract_cong:
  "\<lbrakk> \<And>s s'. \<lbrakk> P s ; s' \<in> P'; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> a s = b s \<rbrakk> \<Longrightarrow>
   ccorres_underlying sr G r xf ar axf P P' hs a c
        = ccorres_underlying sr G r xf ar axf P P' hs b c"
  by (simp add: ccorres_underlying_def split_paired_Ball imp_conjL
          cong: conj_cong xstate.case_cong)

lemma is_aligned_the_x_strengthen:
  "x \<noteq> None \<and> case_option \<top> valid_ipc_buffer_ptr' x s \<longrightarrow> is_aligned (the x) msg_align_bits"
  by (clarsimp simp: valid_ipc_buffer_ptr'_def)

lemma lookupIPCBuffer_Some_0:
  "\<lbrace>\<top>\<rbrace> lookupIPCBuffer w t \<lbrace>\<lambda>rv s. rv \<noteq> Some 0\<rbrace>"
  apply (simp add: lookupIPCBuffer_def
                   ArchVSpace_H.lookupIPCBuffer_def
                   Let_def getThreadBufferSlot_def
                   locateSlot_conv
             cong: if_cong)
  apply wp
   apply simp
  apply (rule hoare_vcg_prop , simp add:hoare_TrueI)
  done

lemma invokeTCB_ReadRegisters_ccorres:
notes
  min_simps [simp del]
shows
  "ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and (\<lambda>s. ksCurThread s = thread) and ct_in_state' (op = Restart)
              and tcb_at' target and sch_act_simple and (\<lambda>s. target \<noteq> ksIdleThread s)
              and (\<lambda>_. target \<noteq> thread))
       (UNIV
            \<inter> {s. tcb_src_' s = tcb_ptr_to_ctcb_ptr target}
            \<inter> {s. suspendSource_' s = from_bool susp}
            \<inter> {s. n_' s = n}
            \<inter> {s. call_' s = from_bool isCall}) []
       (doE reply \<leftarrow> invokeTCB (ReadRegisters target susp n archCp);
           liftE (replyOnRestart thread reply isCall) odE)
       (Call invokeTCB_ReadRegisters_'proc)"
  apply (rule ccorres_gen_asm)
  apply (cinit' lift: tcb_src_' suspendSource_' n_' call_'
                simp: invokeTCB_def liftE_bindE bind_assoc)
   apply (rule ccorres_symb_exec_r)
     apply (rule_tac xf'=thread_' in ccorres_abstract, ceqv)
     apply (rename_tac cthread,
            rule_tac P="cthread = tcb_ptr_to_ctcb_ptr thread" in ccorres_gen_asm2)
     apply (rule ccorres_split_nothrow_dc)
        apply (simp add: when_def del: Collect_const split del: split_if)
        apply (rule ccorres_cond2[where R=\<top>], simp add: from_bool_0 Collect_const_mem)
         apply (ctac add: suspend_ccorres[OF cteDeleteOne_ccorres])
        apply (rule ccorres_return_Skip)
       apply (rule ccorres_pre_getCurThread)
       apply (simp only: liftE_bindE[symmetric])
       apply (ctac add: Arch_performTransfer_ccorres)
          apply (simp add: liftE_bindE Collect_False
                      del: Collect_const)
          apply (simp add: replyOnRestart_def liftE_def bind_assoc when_def
                           replyFromKernel_def if_to_top_of_bind setMRs_def
                           zipWithM_x_mapM_x asUser_mapM_x split_def
                      del: Collect_const cong: if_cong)
          apply (rule ccorres_symb_exec_l)
             apply (rule ccorres_symb_exec_l[OF _ _ _ empty_fail_getThreadState])
               apply (rule ccorres_if_lhs[OF _ ccorres_False[where P'=UNIV]])
               apply (rule ccorres_if_lhs)
                apply (simp add: Collect_True true_def whileAnno_def del: Collect_const)
                apply (rule ccorres_rhs_assoc)+
                apply csymbr
                apply (ctac add: lookupIPCBuffer_ccorres)
                  apply (ctac add: setRegister_ccorres)
                    apply (rule ccorres_stateAssert)
                    apply (rule ccorres_rhs_assoc2)
                    apply (rule_tac P="length reply
                               = min (unat n) (unat n_frameRegisters + unat n_gpRegisters)"
                                in ccorres_gen_asm)
                    apply (rule ccorres_split_nothrow_novcg)
                        apply (rule_tac F="\<lambda>m s. obj_at' (\<lambda>tcb. map (tcbContext tcb) (genericTake n
                                                     (State_H.frameRegisters @ State_H.gpRegisters))
                                                              = reply) target s"
                                   in ccorres_mapM_x_while)
                            apply clarsimp
                            apply (rule ccorres_guard_imp2)
                             apply (rule ccorres_add_return,
                                    ctac add: getRegister_ccorres_defer
                                                [where thread=target])
                               apply (ctac add: setRegister_ccorres)
                              apply wp
                             apply simp
                             apply (vcg exspec=getRegister_modifies)
                            apply (clarsimp simp: getRegister_def submonad_asUser.guarded_gets)
                            apply (clarsimp simp: simpler_gets_def obj_at'_weakenE[OF _ TrueI]
                                                  msg_registers_convs)
                            apply (cut_tac x=na in unat_of_nat32)
                             apply (simp add: word_bits_def n_msgRegisters_def)
                            apply (simp add: msg_registers_convs n_msgRegisters_def
                                             word_of_nat_less)
                            apply (subgoal_tac "na < unat n_frameRegisters")
                             apply (intro conjI[rotated] allI impI)
                               apply (assumption | erule sym)
                              apply (rule frame_gp_registers_convs)
                              apply (simp add: frame_gp_registers_convs)
                             apply (drule obj_at_ko_at')
                             apply (clarsimp simp: obj_at'_def projectKOs asUser_fetch_def
                                                   frame_gp_registers_convs genericTake_def
                                                   nth_append
                                            split: split_if)
                            apply (simp add: n_frameRegisters_def n_msgRegisters_def)
                           apply (simp add: frame_gp_registers_convs msg_registers_convs
                                            n_msgRegisters_def n_frameRegisters_def
                                            n_gpRegisters_def msgMaxLength_def msgLengthBits_def
                                     split: option.split)
                           apply (simp add: min_def word_less_nat_alt split: split_if)[1]
                           apply arith
                          apply (rule allI, rule conseqPre, vcg exspec=setRegister_modifies
                                                                exspec=getRegister_modifies)
                          apply clarsimp
                         apply (wp asUser_obj_at')
                         apply simp
                        apply (simp add: word_bits_def msgMaxLength_def
                                         msg_registers_convs n_msgRegisters_def)
                       apply ceqv
                      (* got to split reply into frameregisters part and gpregisters
                         part remaining, match against 2nd and 4th loop. 3rd loop
                         never executes with current configuration *)
                      apply (simp add: msg_registers_convs del: Collect_const)
                      apply (rule iffD2 [OF ccorres_abstract_cong])
                       apply (rule bind_apply_cong[OF _ refl])
                       apply (rule_tac n1="min (unat n_frameRegisters - unat n_msgRegisters) (unat n)"
                                   in fun_cong [OF mapM_x_split_append])
                      apply (rule_tac P="rva \<noteq> Some 0" in ccorres_gen_asm)
                      apply (subgoal_tac "(ipcBuffer = NULL) = (rva = None)")
                       prefer 2
                       apply (clarsimp simp: option_to_ptr_def option_to_0_def
                                      split: option.split_asm)
                      apply (simp add: bind_assoc del: Collect_const)
                      apply (rule_tac xf'=i_' and r'="\<lambda>_ rv. unat rv = min (unat n_frameRegisters)
                                                                      (min (unat n)
                                                                           (case rva of None \<Rightarrow> unat n_msgRegisters
                                                                              | _ \<Rightarrow> unat n_frameRegisters))"
                                 in ccorres_split_nothrow_novcg)
                          apply (rule ccorres_Cond_rhs)
                           apply (simp del: Collect_const)
                           apply (rule ccorres_rel_imp,
                                  rule_tac F="\<lambda>m s. obj_at' (\<lambda>tcb. map (tcbContext tcb) (genericTake n
                                                      (State_H.frameRegisters @ State_H.gpRegisters))
                                                               = reply) target s
                                                 \<and> is_aligned (the rva) msg_align_bits \<and> valid_pspace' s"
                                       and i="unat n_msgRegisters"
                                    in ccorres_mapM_x_while')
                                apply (clarsimp simp: less_diff_conv)
                                apply (rule ccorres_guard_imp2)
                                 apply (rule ccorres_add_return,
                                        ctac add: getRegister_ccorres_defer[where thread=target])
                                   apply (rule storeWordUser_ccorres)
                                  apply wp
                                 apply (vcg exspec=getRegister_modifies)
                                apply (clarsimp simp: obj_at'_weakenE[OF _ TrueI]
                                                      word_size)
                                apply (intro conjI[rotated] impI allI)
                                     apply (simp add: n_msgRegisters_def n_frameRegisters_def
                                                      word_less_nat_alt)
                                     apply (subst unat_add_lem[THEN iffD1], simp_all add: unat_of_nat)[1]
                                    apply (erule sym)
                                   apply (simp add: option_to_ptr_def option_to_0_def
                                                    msg_registers_convs upto_enum_word
                                              del: upt.simps)
                                  apply (rule frame_gp_registers_convs)
                                  apply (simp add: frame_gp_registers_convs less_diff_conv)
                                  apply (subst iffD1 [OF unat_add_lem])
                                   apply (simp add: n_msgRegisters_def n_frameRegisters_def

                                                    word_le_nat_alt unat_of_nat)
                                  apply (simp add: n_frameRegisters_def n_msgRegisters_def
                                                   unat_of_nat)
                                 apply (erule aligned_add_aligned)
                                   apply (simp add: word32_shift_by_2 is_aligned_shiftl_self)
                                 apply (simp add: msg_align_bits)
                                apply (clarsimp simp: getRegister_def submonad_asUser.guarded_gets
                                                      obj_at'_weakenE[OF _ TrueI])
                                apply (clarsimp simp: asUser_fetch_def simpler_gets_def
                                                      obj_at'_def projectKOs genericTake_def
                                                      nth_append frame_gp_registers_convs)
                                apply (simp add: n_msgRegisters_def unat_of_nat n_frameRegisters_def)
                                apply (subst iffD1 [OF unat_add_lem])
                                 apply (simp add: unat_of_nat)+
                               apply (clarsimp simp: less_diff_conv)
                               apply (simp add: frame_gp_registers_convs msg_registers_convs
                                                n_msgRegisters_def n_frameRegisters_def
                                                n_gpRegisters_def Types_H.msgMaxLength_def
                                                Types_H.msgLengthBits_def
                                         split: option.split)
                               apply (simp add: min_def word_less_nat_alt split: split_if)[1]
                               apply (simp split: split_if_asm, arith+)[1]
                              apply (rule allI, rule conseqPre, vcg)
                              apply clarsimp
                             apply (wp)
                            apply (clarsimp simp: less_diff_conv)
                            apply (simp add: word_bits_def n_msgRegisters_def n_frameRegisters_def
                                             Types_H.msgLengthBits_def Types_H.msgMaxLength_def
                                             msg_registers_convs)
                           apply (clarsimp simp: n_msgRegisters_def n_frameRegisters_def
                                                 msgMaxLength_def Types_H.msgLengthBits_def
                                                 n_gpRegisters_def msg_registers_convs
                                          split: option.split_asm)
                           apply (simp add: min_def split: split_if_asm split_if)
                           apply arith
                          apply (drule_tac s=rv'a in sym, simp)
                          apply (rule_tac P=\<top> and P'="{s. i_' s = rv'a}" in ccorres_inst)
                          apply clarsimp
                          apply (elim disjE impCE)
                            apply (clarsimp simp: word_le_nat_alt linorder_not_less)
                            apply (subst (asm) unat_of_nat32)
                             apply (simp add: n_msgRegisters_def word_bits_def)
                            apply (clarsimp simp: mapM_x_Nil)
                            apply (rule ccorres_guard_imp2, rule ccorres_return_Skip')
                            apply (simp add: n_msgRegisters_def n_frameRegisters_def
                                             n_gpRegisters_def cong: option.case_cong)
                            apply (simp add: min_def split: split_if option.split)
                           apply (simp add: mapM_x_Nil)
                           apply (rule ccorres_guard_imp2, rule ccorres_return_Skip')
                           apply (simp add: n_msgRegisters_def n_frameRegisters_def
                                            n_gpRegisters_def cong: option.case_cong)
                           apply (simp add: min_def split: split_if option.split)
                           apply (clarsimp simp only: unat_arith_simps, simp)
                          apply (clarsimp simp: less_diff_conv word_le_nat_alt linorder_not_less)
                          apply (subst(asm) unat_of_nat32)
                           apply (simp add: word_bits_def n_msgRegisters_def)
                          apply (simp add: mapM_x_Nil n_frameRegisters_def n_gpRegisters_def)
                          apply (rule ccorres_guard_imp2, rule ccorres_return_Skip')
                          apply (simp add: n_msgRegisters_def n_frameRegisters_def
                                           n_gpRegisters_def cong: option.case_cong)
                         apply ceqv
                        apply csymbr
                        apply csymbr
                        apply (rule iffD1[OF ccorres_expand_while_iff_Seq])
                        apply (rule ccorres_cond_false)
                        apply (rule ccorres_split_nothrow_novcg)
                            apply (rule_tac xf'=i_' in ccorres_abstract, ceqv)
                            apply (rename_tac i_c, rule_tac P="i_c = 0" in ccorres_gen_asm2)
                            apply (simp add: drop_zip del: Collect_const)
                            apply (rule ccorres_Cond_rhs)
                             apply (simp del: Collect_const)
                             apply (rule_tac F="\<lambda>m s. obj_at' (\<lambda>tcb. map (tcbContext tcb) (genericTake n
                                                       (State_H.frameRegisters @ State_H.gpRegisters))
                                                                = reply) target s
                                                  \<and> is_aligned (the rva) msg_align_bits \<and> valid_pspace' s"
                                        and i="0" in ccorres_mapM_x_while')
                                 apply (clarsimp simp: less_diff_conv drop_zip)
                                 apply (rule ccorres_guard_imp2)
                                  apply (rule ccorres_add_return,
                                         ctac add: getRegister_ccorres_defer[where thread=target])
                                    apply (rule storeWordUser_ccorres)
                                   apply wp
                                  apply (vcg exspec=getRegister_modifies)
                                 apply (clarsimp simp: obj_at'_weakenE[OF _ TrueI]
                                                       word_size)
                                 apply (intro conjI[rotated] impI allI)
                                      apply (simp add: n_frameRegisters_def n_msgRegisters_def
                                                       length_msgRegisters word_of_nat_less
                                                       n_gpRegisters_def)
                                     apply (erule sym)
                                    apply (simp add: option_to_ptr_def option_to_0_def
                                                     msg_registers_convs upto_enum_word
                                                     n_msgRegisters_def n_frameRegisters_def
                                                     n_gpRegisters_def msgMaxLength_def msgLengthBits_def
                                                del: upt.simps upt_rec_numeral)
                                    apply (simp add: min_def split: split_if_asm)
                                   apply (rule frame_gp_registers_convs)
                                   apply (simp add: frame_gp_registers_convs n_msgRegisters_def n_frameRegisters_def
                                                    n_gpRegisters_def msgMaxLength_def msgLengthBits_def
                                                    unat_of_nat)
                                  apply (erule aligned_add_aligned)
                                    apply (simp add: word32_shift_by_2 is_aligned_shiftl_self)
                                  apply (simp add: msg_align_bits)
                                 apply (clarsimp simp: getRegister_def submonad_asUser.guarded_gets
                                                       obj_at'_weakenE[OF _ TrueI])
                                 apply (clarsimp simp: asUser_fetch_def simpler_gets_def
                                                       obj_at'_def projectKOs genericTake_def
                                                       nth_append frame_gp_registers_convs
                                                       n_frameRegisters_def n_gpRegisters_def
                                                       n_msgRegisters_def frame_gp_registers_convs
                                                 cong: if_cong split: split_if)
                                 apply (clarsimp simp: frame_gp_registers_convs n_gpRegisters_def
                                                       min.absorb1 unat_of_nat)
                                apply (clarsimp simp: less_diff_conv)
                                apply (clarsimp simp: nth_append frame_gp_registers_convs
                                                      n_frameRegisters_def n_gpRegisters_def
                                                      n_msgRegisters_def frame_gp_registers_convs
                                                      Types_H.msgMaxLength_def Types_H.msgLengthBits_def
                                                      msg_registers_convs
                                                cong: if_cong split: split_if)
                                apply (simp add: word_less_nat_alt unat_of_nat)
                                apply (simp add: iffD1[OF unat_add_lem] cong: conj_cong)
                                apply (simp add: min_def
                                          split: split_if split_if_asm, arith+)[1]
                               apply (rule allI, rule conseqPre, vcg)
                               apply clarsimp
                              apply wp
                             apply (simp add: word_bits_def n_frameRegisters_def n_gpRegisters_def
                                              n_msgRegisters_def)
                             apply (simp add: min_less_iff_disj less_imp_diff_less)
                            apply (simp add: drop_zip n_gpRegisters_def)
                            apply (elim disjE impCE)
                             apply (clarsimp simp: mapM_x_Nil)
                             apply (rule ccorres_return_Skip')
                            apply (simp add: linorder_not_less word_le_nat_alt
                                             drop_zip mapM_x_Nil n_frameRegisters_def
                                             min.absorb1 n_msgRegisters_def)
                            apply (rule ccorres_guard_imp2, rule ccorres_return_Skip')
                            apply simp
                           apply ceqv
                          apply csymbr
                          apply (rule ccorres_rhs_assoc2)
                          apply (ctac (no_vcg) add: setMessageInfo_ccorres)
                            apply (ctac (no_vcg))
                             apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
                             apply (rule allI, rule conseqPre, vcg)
                             apply (clarsimp simp: return_def)
                            apply (wp | simp add: valid_tcb_state'_def)+
                          apply (clarsimp simp: ThreadState_Running_def mask_def)
                         apply (rule mapM_x_wp')
                         apply (rule hoare_pre)
                          apply (wp sch_act_wf_lift valid_queues_lift tcb_in_cur_domain'_lift)
                         apply clarsimp
                        apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem)
                        apply (simp add: message_info_to_H_def)
                        apply (clarsimp simp: n_frameRegisters_def n_msgRegisters_def 
                                              n_gpRegisters_def field_simps upto_enum_word
                                              word_less_nat_alt Types_H.msgMaxLength_def
                                              Types_H.msgLengthBits_def 
                                    simp del: upt.simps
                                       split: option.split_asm)
                         apply (clarsimp simp: min_def iffD2 [OF mask_eq_iff_w2p] word_size
                                               word_less_nat_alt
                                       split: split_if_asm dest!: word_unat.Rep_inverse')
                        apply (clarsimp simp: length_msgRegisters n_msgRegisters_def)
                        apply (clarsimp simp: min_def iffD2 [OF mask_eq_iff_w2p] word_size
                                              word_less_nat_alt 
                                      split: split_if_asm dest!: word_unat.Rep_inverse')
                        apply unat_arith
                       apply simp
                       apply (wp mapM_x_wp' sch_act_wf_lift valid_queues_lift static_imp_wp
                                 tcb_in_cur_domain'_lift)
                      apply (simp add: n_frameRegisters_def n_msgRegisters_def
                                       guard_is_UNIV_def)
                     apply simp
                     apply (rule mapM_x_wp')
                     apply (rule hoare_pre)
                      apply (wp asUser_obj_at'[where t'=target] static_imp_wp)
                     apply clarsimp
                    apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem
                                          msg_registers_convs n_msgRegisters_def
                                          n_frameRegisters_def n_gpRegisters_def
                                          msgMaxLength_def msgLengthBits_def
                                          word_less_nat_alt unat_of_nat)
                    apply (simp add: min_def split: split_if_asm)
                   apply (wp_once hoare_drop_imps)
                   apply (wp asUser_obj_at'[where t'=target] static_imp_wp)
                  apply (vcg exspec=setRegister_modifies)
                 apply simp
                 apply (strengthen is_aligned_the_x_strengthen)
                 apply simp
                 apply (wp lookupIPCBuffer_Some_0 | wp_once hoare_drop_imps)+
                apply (simp add: Collect_const_mem State_H.badgeRegister_def
                                 ARMMachineTypes.badgeRegister_def
                                 "StrictC'_register_defs")
                apply (vcg exspec=lookupIPCBuffer_modifies)
               apply (simp add: false_def)
               apply (ctac(no_vcg) add: setThreadState_ccorres)
                apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV])
                apply (rule allI, rule conseqPre, vcg)
                apply (simp add: return_def)
               apply wp
             apply (simp cong: rev_conj_cong)
             apply wp
            apply (wp asUser_inv mapM_wp' getRegister_inv
                      asUser_get_registers static_imp_wp)
            apply (rule hoare_strengthen_post, rule asUser_get_registers)
            apply (clarsimp simp: obj_at'_def genericTake_def
                                  frame_gp_registers_convs)
            apply arith
           apply (wp static_imp_wp)
          apply simp
         apply (rule ccorres_inst[where P=\<top> and P'=UNIV], simp)
        apply (simp add: performTransfer_def)
        apply wp
       apply (simp add: Collect_const_mem "StrictC'_thread_state_defs"
                        mask_def)
       apply vcg
      apply (rule_tac Q="\<lambda>rv. invs' and st_tcb_at' (op = Restart) thread
                             and tcb_at' target" in hoare_post_imp)
       apply (clarsimp simp: st_tcb_at_tcb_at')
       apply (auto elim!: st_tcb'_weakenE)[1]
      apply (wp suspend_st_tcb_at')
     apply (vcg exspec=suspend_modifies)
    apply vcg
   apply (rule conseqPre, vcg, clarsimp)
  apply (clarsimp simp: rf_sr_ksCurThread ct_in_state'_def 
                 split: split_if)
  done

lemma capTCBPtr_eq:
  "\<lbrakk> ccap_relation cap cap'; isThreadCap cap \<rbrakk>
     \<Longrightarrow> cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap')
           = ptr_val (tcb_ptr_to_ctcb_ptr (capTCBPtr cap))"
  apply (simp add: cap_get_tag_isCap[symmetric])
  apply (drule(1) cap_get_tag_to_H)
  apply clarsimp
  done

lemma decodeReadRegisters_ccorres:
  "ccorres (intr_and_se_rel \<currency> dc)  (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active'
              and sysargs_rel args buffer
              and tcb_at' (capTCBPtr cp) and ex_nonz_cap_to' (capTCBPtr cp)
              and K (isThreadCap cp))
       (UNIV
            \<inter> {s. ccap_relation cp (cap_' s)}
            \<inter> {s. unat (length_' s) = length args}
            \<inter> {s. call_' s = from_bool isCall}
            \<inter> {s. buffer_' s = option_to_ptr buffer}) []
     (decodeReadRegisters args cp
            >>= invocationCatch thread isBlocking isCall InvokeTCB)
     (Call decodeReadRegisters_'proc)"
  apply (cinit' lift: cap_' length_' call_' buffer_')
   apply (simp add: decodeReadRegisters_def decodeTransfer_def
               del: Collect_const cong: list.case_cong)
   apply wpc
    apply (drule word_unat.Rep_inverse')
    apply (simp add: throwError_bind invocationCatch_def
               cong: StateSpace.state.fold_congs globals.fold_congs)
    apply (rule syscall_error_throwError_ccorres_n)
    apply (simp add: syscall_error_to_H_cases)
   apply wpc
    apply (drule word_unat.Rep_inverse')
    apply (simp add: throwError_bind invocationCatch_def
               cong: StateSpace.state.fold_congs globals.fold_congs)
    apply (rule syscall_error_throwError_ccorres_n)
    apply (simp add: syscall_error_to_H_cases)
   apply (simp add: word_less_nat_alt Collect_False del: Collect_const)
   apply (rule ccorres_add_return,
          ctac add: getSyscallArg_ccorres_foo[where args=args and n=0 and buffer=buffer])
     apply (rule ccorres_add_return,
            ctac add: getSyscallArg_ccorres_foo[where args=args and n=1 and buffer=buffer])
       apply (rule ccorres_move_const_guards)+
       apply (simp add: rangeCheck_def unlessE_whenE whenE_def if_to_top_of_bindE
                        ccorres_seq_cond_raise if_to_top_of_bind
                   del: Collect_const)
       apply (rule ccorres_cond2[where R=\<top>])
         apply (simp add: frame_gp_registers_convs n_frameRegisters_def
                          n_gpRegisters_def Collect_const_mem)
         apply unat_arith
        apply (simp add: throwError_bind invocationCatch_def
                   cong: StateSpace.state.fold_congs globals.fold_congs)
        apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
         apply vcg
        apply (rule conseqPre, vcg)
        apply (clarsimp simp: throwError_def return_def intr_and_se_rel_def
                              syscall_error_rel_def syscall_error_to_H_cases
                              exception_defs Collect_const_mem)
        apply (simp add: frame_gp_registers_convs n_frameRegisters_def
                         n_gpRegisters_def)
       apply (simp add: ccorres_invocationCatch_Inr returnOk_bind
                        performInvocation_def
                   del: Collect_const)
       apply (rule ccorres_Guard_Seq)+
       apply csymbr
       apply csymbr
       apply csymbr
       apply (simp add: liftE_bindE bind_assoc)
       apply (rule ccorres_pre_getCurThread)
       apply (rule ccorres_cond_seq)
       apply (rule_tac R="\<lambda>s. rv = ksCurThread s \<and> isThreadCap cp" and P="\<lambda>s. capTCBPtr cp = rv" in ccorres_cond_both)
         apply clarsimp
         apply (frule rf_sr_ksCurThread)
         apply clarsimp
         apply (frule (1) cap_get_tag_isCap[symmetric, THEN iffD1])
         apply (drule (1) cap_get_tag_to_H)
         apply clarsimp
         apply (rule iffI)
          apply (drule_tac t="ksCurThread s" in sym)
          apply simp
         apply simp
        apply (rule_tac P="capTCBPtr cp = rv" in ccorres_gen_asm)
        apply simp
        apply (simp add: throwError_bind invocationCatch_def
                    cong: StateSpace.state.fold_congs globals.fold_congs)
        apply (rule syscall_error_throwError_ccorres_n)
        apply (simp add: syscall_error_to_H_cases)
       apply (rule_tac P="capTCBPtr cp \<noteq> rv" in ccorres_gen_asm)
       apply (simp add: returnOk_bind)
       apply (simp add: ccorres_invocationCatch_Inr del: Collect_const)
       apply (ctac add: setThreadState_ccorres)
         apply csymbr
         apply (rule ccorres_Guard_Seq)+
         apply (rule ccorres_nondet_refinement)
          apply (rule is_nondet_refinement_bindE)
           apply (rule is_nondet_refinement_refl)
          apply (simp split: split_if)
          apply (rule conjI[rotated], rule impI, rule is_nondet_refinement_refl)
          apply (rule impI)
          apply (rule is_nondet_refinement_alternative1)         
         apply (simp add: performInvocation_def)
         apply (rule ccorres_add_returnOk)
         apply (ctac(no_vcg) add: invokeTCB_ReadRegisters_ccorres)
           apply (rule ccorres_return_CE, simp+)[1]
          apply (rule ccorres_return_C_errorE, simp+)[1]
         apply wp
        apply (wp ct_in_state'_set sts_invs_minor')
       apply (simp add: Collect_const_mem intr_and_se_rel_def
                        cintr_def exception_defs)
       apply (vcg exspec=setThreadState_modifies)
      apply wp
     apply (vcg exspec=getSyscallArg_modifies)
    apply wp
   apply (vcg exspec=getSyscallArg_modifies)
  apply (clarsimp simp: Collect_const_mem rf_sr_ksCurThread
                        "StrictC'_thread_state_defs" word_sless_def word_sle_def
                        mask_eq_iff_w2p word_size isCap_simps
                        ReadRegistersFlags_defs tcb_at_invs'
                        cap_get_tag_isCap capTCBPtr_eq)
  apply (frule global'_no_ex_cap[OF invs_valid_global'], clarsimp)
  apply (rule conjI)
   apply clarsimp
   apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def)
   apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def)
   apply (auto simp: ct_in_state'_def n_frameRegisters_def n_gpRegisters_def
                     valid_tcb_state'_def
              elim!: st_tcb'_weakenE
              dest!: st_tcb_at_idle_thread')[1]
  apply (clarsimp simp: from_bool_def word_and_1 split: split_if)
  done

lemma decodeWriteRegisters_ccorres:
  "ccorres (intr_and_se_rel \<currency> dc)  (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and sch_act_simple 
              and (\<lambda>s. ksCurThread s = thread) and ct_active' and K (isThreadCap cp)
              and valid_cap' cp and (\<lambda>s. \<forall>x \<in> zobj_refs' cp. ex_nonz_cap_to' x s)
              and sysargs_rel args buffer)
       (UNIV
            \<inter> {s. ccap_relation cp (cap_' s)}
            \<inter> {s. unat (length_' s) = length args}
            \<inter> {s. buffer_' s = option_to_ptr buffer}) []
     (decodeWriteRegisters args cp
            >>= invocationCatch thread isBlocking isCall InvokeTCB)
     (Call decodeWriteRegisters_'proc)"
  apply (cinit' lift: cap_' length_' buffer_' simp: decodeWriteRegisters_def) 
   apply (rename_tac length' cap')
   apply (rule ccorres_Cond_rhs_Seq)
    apply wpc
     apply (simp add: throwError_bind invocationCatch_def
                cong: StateSpace.state.fold_congs globals.fold_congs)
     apply (rule syscall_error_throwError_ccorres_n)
     apply (simp add: syscall_error_to_H_cases)
    apply (simp add: word_less_nat_alt)
    apply (simp add: throwError_bind invocationCatch_def
               cong: StateSpace.state.fold_congs globals.fold_congs)
    apply (rule syscall_error_throwError_ccorres_n)
    apply (simp add: syscall_error_to_H_cases)
   apply (simp add: word_less_nat_alt del: Collect_const)
   apply (rule_tac P="\<lambda>a. ccorres rvr xf P P' hs a c" for rvr xf P P' hs c in ssubst,
          rule bind_cong [OF _ refl], rule list_case_helper,
          clarsimp simp: tl_drop_1)+
   apply (rule ccorres_add_return)
   apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n=0 and buffer=buffer])
     apply (rule ccorres_add_return)
     apply (ctac add: getSyscallArg_ccorres_foo[where args=args and n=1 and buffer=buffer])
       apply (rule_tac P="unat (of_nat (length args) :: word32) = length args"
                    in ccorres_gen_asm)
       apply (simp add: unat_sub word_le_nat_alt genericLength_def
                        word_less_nat_alt hd_drop_conv_nth2 tl_drop_1
                   del: Collect_const)
       apply (rule ccorres_Cond_rhs_Seq)
        apply (simp add: whenE_def throwError_bind invocationCatch_def
                   cong: StateSpace.state.fold_congs globals.fold_congs)
        apply (rule syscall_error_throwError_ccorres_n)
        apply (simp add: syscall_error_to_H_cases)
       apply (simp add: whenE_def decodeTransfer_def returnOk_bind del: Collect_const)
       apply (rule ccorres_Guard_Seq)+
       apply csymbr
       apply csymbr
       apply csymbr
       apply (simp add: liftE_bindE bind_assoc)
       apply (rule ccorres_pre_getCurThread)
       apply (rule ccorres_cond_seq) 
       apply (rule_tac R="\<lambda>s. rv = ksCurThread s \<and> isThreadCap cp" and P="\<lambda>s. capTCBPtr cp = rv" in ccorres_cond_both)
         apply clarsimp
         apply (frule rf_sr_ksCurThread)
         apply clarsimp
         apply (frule (1) cap_get_tag_isCap[symmetric, THEN iffD1])
         apply (drule (1) cap_get_tag_to_H)
         apply clarsimp
         apply (rule iffI)
          apply (drule_tac t="ksCurThread s" in sym)
          apply simp
         apply simp
        apply (rule_tac P="capTCBPtr cp = rv" in ccorres_gen_asm)
        apply simp
        apply (simp add: throwError_bind invocationCatch_def
                    cong: StateSpace.state.fold_congs globals.fold_congs)
        apply (rule syscall_error_throwError_ccorres_n)
        apply (simp add: syscall_error_to_H_cases)
       apply (rule_tac P="capTCBPtr cp \<noteq> rv" in ccorres_gen_asm)
       apply (simp add: returnOk_bind)
       apply (simp add: ccorres_invocationCatch_Inr del: Collect_const)
       apply (ctac add: setThreadState_ccorres)
         apply (rule ccorres_Guard_Seq)+
         apply (simp add: performInvocation_def)
         apply (ctac(no_vcg) add: invokeTCB_WriteRegisters_ccorres
                                    [where args=args and someNum="unat (args ! 1)"])
           apply (simp add: dc_def[symmetric] o_def)
           apply (rule ccorres_alternative2, rule ccorres_return_CE, simp+)
          apply (rule ccorres_return_C_errorE, simp+)[1]
         apply wp[1]
        apply simp
        apply (wp sts_invs_minor' setThreadState_sysargs_rel)
       apply (simp add: Collect_const_mem cintr_def intr_and_se_rel_def
                        exception_defs)
       apply (vcg exspec=setThreadState_modifies)
      apply wp
     apply (vcg exspec=getSyscallArg_modifies)
    apply wp
   apply (vcg exspec=getSyscallArg_modifies)
  apply (clarsimp simp: Collect_const_mem ct_in_state'_def st_tcb_at_tcb_at')
  apply (simp add: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
  apply (clarsimp simp: valid_cap'_def "StrictC'_thread_state_defs"
                        mask_eq_iff_w2p word_size rf_sr_ksCurThread
                        WriteRegisters_resume_def word_sle_def word_sless_def
                        numeral_eqs)
  apply (frule arg_cong[where f="\<lambda>x. unat (of_nat x :: word32)"],
         simp(no_asm_use) only: word_unat.Rep_inverse o_def,
         simp)
  apply (rule conjI)
   apply clarsimp
   apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def word_less_nat_alt)
   apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def word_less_nat_alt)
   apply (auto simp: genericTake_def cur_tcb'_def linorder_not_less word_le_nat_alt
                     valid_tcb_state'_def
              elim!: st_tcb'_weakenE dest!: st_tcb_at_idle_thread')[1]   
  apply (intro allI impI)
  apply (rule disjCI2)
  apply (clarsimp simp: genericTake_def linorder_not_less)
  apply (subst hd_conv_nth, clarsimp simp: unat_eq_0)
  apply (clarsimp simp: from_bool_def word_and_1
                 split: split_if)
  done

lemma excaps_map_Nil: "(excaps_map caps = []) = (caps = [])"
  by (simp add: excaps_map_def)

(* FIXME: move *)
lemma and_eq_0_is_nth:
  fixes x :: "('a :: len) word"
  shows "y = 1 << n \<Longrightarrow> ((x && y) = 0) = (\<not> (x !! n))"
  by (metis (poly_guards_query) and_eq_0_is_nth)

(* FIXME: move *)
lemmas and_neq_0_is_nth = arg_cong [where f=Not, OF and_eq_0_is_nth, simplified]

lemma decodeCopyRegisters_ccorres:
  "interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
   ccorres (intr_and_se_rel \<currency> dc)  (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and sch_act_simple 
              and (\<lambda>s. ksCurThread s = thread) and ct_active'
              and (excaps_in_mem extraCaps o ctes_of)
              and (\<lambda>s. \<forall>v \<in> set extraCaps.
                             ex_cte_cap_wp_to' isCNodeCap (snd v) s)
              and tcb_at' (capTCBPtr cp) and ex_nonz_cap_to' (capTCBPtr cp)
              and (\<lambda>s. \<forall>v \<in> set extraCaps. \<forall>y \<in> zobj_refs' (fst v).
                              ex_nonz_cap_to' y s)
              and sysargs_rel args buffer
              and K (isThreadCap cp))
       (UNIV
            \<inter> {s. ccap_relation cp (cap_' s)}
            \<inter> {s. unat (length_' s) = length args}
            \<inter> {s. extraCaps_' s = extraCaps'}
            \<inter> {s. buffer_' s = option_to_ptr buffer}) []
     (decodeCopyRegisters args cp (map fst extraCaps)
            >>= invocationCatch thread isBlocking isCall InvokeTCB)
     (Call decodeCopyRegisters_'proc)"
  apply (cinit' lift: cap_' length_' extraCaps_' buffer_' simp: decodeCopyRegisters_def)
   apply csymbr
   apply wpc
    apply (simp add: if_1_0_0 unat_eq_0)
    apply (rule ccorres_cond_true_seq)
    apply (simp add: invocationCatch_def throwError_bind
               cong: StateSpace.state.fold_congs globals.fold_congs)
    apply (rule syscall_error_throwError_ccorres_n)
    apply (simp add: syscall_error_to_H_cases)
   apply (simp add: if_1_0_0 del: Collect_const)
   apply (subst unat_eq_0[symmetric], simp add: Collect_False del: Collect_const)
   apply (rule ccorres_Guard_Seq)+
   apply csymbr
   apply (simp add: if_1_0_0 interpret_excaps_test_null decodeTransfer_def
               del: Collect_const)
   apply (rule ccorres_Cond_rhs_Seq)
    apply (simp add: excaps_map_def invocationCatch_def throwError_bind null_def
               cong: StateSpace.state.fold_congs globals.fold_congs)
    apply (rule syscall_error_throwError_ccorres_n)
    apply (simp add: syscall_error_to_H_cases)
   apply (simp add: excaps_map_def null_def del: Collect_const)
   apply (rule ccorres_add_return,
          ctac add: getSyscallArg_ccorres_foo[where args=args and n=0 and buffer=buffer])
     apply (rule ccorres_Guard_Seq)+
     apply (rule ccorres_symb_exec_r)
       apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=0])
       apply (rule ccorres_move_c_guard_cte)
       apply ctac
         apply csymbr
         apply (simp add: cap_get_tag_isCap if_1_0_0 del: Collect_const)
         apply (rule ccorres_assert2)
         apply (rule ccorres_Cond_rhs_Seq)
          apply (rule_tac P="Q' (capTCBPtr rva) rva" for Q'
                     in ccorres_inst)
          apply (rule ccorres_rhs_assoc)+
          apply (csymbr, csymbr)
          apply (simp add: hd_map del: Collect_const,
                 simp add: hd_conv_nth del: Collect_const)
          apply (simp only: cap_get_tag_isCap[symmetric],
                 drule(1) cap_get_tag_to_H)
          apply (simp add: case_bool_If if_to_top_of_bindE
                           if_to_top_of_bind
                      del: Collect_const cong: if_cong)
          apply (simp add: to_bool_def returnOk_bind Collect_True
                           ccorres_invocationCatch_Inr performInvocation_def
                      del: Collect_const) 
          apply (ctac add: setThreadState_ccorres)
            apply csymbr
            apply (rule ccorres_Guard_Seq)+
            apply (ctac add: invokeTCB_CopyRegisters_ccorres)
               apply simp
               apply (rule ccorres_alternative2)
               apply (rule ccorres_return_CE, simp+)[1]
              apply (rule ccorres_return_C_errorE, simp+)[1]
             apply wp
            apply (simp add: cintr_def intr_and_se_rel_def exception_defs)
            apply (vcg exspec=invokeTCB_CopyRegisters_modifies)
           apply (wp sts_invs_minor')
          apply (simp add: Collect_const_mem)
          apply (vcg exspec=setThreadState_modifies)
         apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
          apply vcg
         apply (rule conseqPre, vcg)
         apply (simp add: hd_map isCap_simps hd_conv_nth)
         apply (clarsimp simp: invocationCatch_def throwError_bind
                        split: capability.split,
                auto simp: throwError_def return_def intr_and_se_rel_def
                           syscall_error_rel_def syscall_error_to_H_cases
                           exception_defs)[1]
        apply (simp add: getSlotCap_def)
        apply (wp getCTE_wp)
       apply (simp add: Collect_const_mem if_1_0_0 cap_get_tag_isCap)
       apply vcg
      apply (simp add: Collect_const_mem)
      apply vcg
     apply (rule conseqPre, vcg)
     apply clarsimp
    apply wp
   apply (simp add: Collect_const_mem)
   apply (vcg exspec=getSyscallArg_modifies)
  apply (clarsimp simp: Collect_const_mem excaps_map_Nil)
  apply (rule conjI)
   apply (clarsimp simp: excaps_in_mem_def neq_Nil_conv
                         slotcap_in_mem_def cte_wp_at_ctes_of
                         ct_in_state'_def st_tcb_at_tcb_at')
   apply (rule conjI)
    apply (clarsimp simp: sysargs_rel_n_def n_msgRegisters_def)
   apply (cut_tac msk=ba and cap="cteCap cte" in capMasterCap_maskCapRights)
   apply (clarsimp simp: isCap_simps simp del: capMasterCap_maskCapRights)
   apply (frule ctes_of_valid', clarsimp+)
   apply (auto simp: valid_cap'_def excaps_map_def valid_tcb_state'_def
              elim!: st_tcb'_weakenE
              dest!: st_tcb_at_idle_thread' interpret_excaps_eq)[1]
  apply (clarsimp simp: word_sle_def CopyRegistersFlags_defs word_sless_def
                        "StrictC'_thread_state_defs" rf_sr_ksCurThread
                 split: split_if)
  apply (drule interpret_excaps_eq)
  apply (clarsimp simp: mask_def excaps_map_def split_def ccap_rights_relation_def
                        rightsFromWord_wordFromRights excaps_map_Nil)
  apply (simp only: cap_get_tag_isCap[symmetric],
         drule(1) cap_get_tag_to_H)
  apply (clarsimp simp: cap_get_tag_isCap to_bool_def)
  apply (auto simp: unat_eq_of_nat word_and_1_shiftls
    word_and_1_shiftl [where n=3,simplified] cap_get_tag_isCap[symmetric] split: split_if_asm)
  done

(* FIXME: move *)
lemma ucast_le_ucast_8_32:
  "(ucast x \<le> (ucast y :: word32)) = (x \<le> (y :: word8))"
  by (simp add: word_le_nat_alt)

(* FIXME: move *)
lemma ccap_relation_gen_framesize_to_H:
  "\<lbrakk> ccap_relation cap cap'; isArchPageCap cap \<rbrakk>
       \<Longrightarrow> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap'))
                 = capVPSize (capCap cap)"
  apply (clarsimp simp: isCap_simps)
  apply (case_tac "sz = ARMMachineTypes.ARMSmallPage")
   apply (frule cap_get_tag_PageCap_small_frame)
   apply (simp add: cap_get_tag_isCap isCap_simps
                    pageSize_def cap_lift_small_frame_cap
                    generic_frame_cap_get_capFSize_CL_def
                    gen_framesize_to_H_def)
  apply (subgoal_tac "cap_get_tag cap' = scast cap_frame_cap")
   apply (frule(1) iffD1 [OF cap_get_tag_PageCap_frame])
   apply (clarsimp simp: cap_frame_cap_lift generic_frame_cap_get_capFSize_CL_def)
   apply (simp add: gen_framesize_to_H_def framesize_to_H_def
             split: split_if)
   apply (clarsimp simp: ccap_relation_def c_valid_cap_def
                         cl_valid_cap_def)
  apply (simp add: cap_get_tag_isCap isCap_simps pageSize_def)
  done

lemma checkValidIPCBuffer_ccorres:
  "ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs') (UNIV \<inter> {s. vptr_' s = vptr} \<inter> {s. ccap_relation cp (cap_' s)}) []
       (checkValidIPCBuffer vptr cp)
       (Call checkValidIPCBuffer_'proc)"
  apply (cases "isArchPageCap cp")
   apply (simp only: isCap_simps, safe)[1]
   apply (cinit lift: vptr_' cap_')
    apply (simp add: ArchVSpace_H.checkValidIPCBuffer_def del: Collect_const)
    apply (csymbr, csymbr)
    apply (simp add: cap_get_tag_isCap if_1_0_0 isCap_simps del: Collect_const)
    apply (rule ccorres_add_return,
           rule_tac xf'=ret__int_' and r'="\<lambda>rv rv'. rv' = 0" in ccorres_split_nothrow)
        apply (rule ccorres_Cond_rhs)
         apply csymbr
         apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV])
         apply (rule allI, rule conseqPre, vcg)
         apply (clarsimp simp add: return_def cap_get_tag_isCap isCap_simps)
        apply (rule ccorres_return_Skip')
       apply ceqv
      apply (simp add: Collect_False del: Collect_const)
      apply (rule ccorres_Guard_Seq)+
      apply (simp add: whenE_def ccorres_seq_cond_raise
                       if_to_top_of_bindE del: Collect_const)
      apply (rule ccorres_cond2[where R=\<top>])
        apply (simp add: mask_def Collect_const_mem msgAlignBits_def)
       apply (simp cong: StateSpace.state.fold_congs globals.fold_congs)
       apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
        apply vcg
       apply (rule conseqPre, vcg)
       apply (clarsimp simp: throwError_def return_def exception_defs
                             syscall_error_rel_def syscall_error_to_H_cases)
      apply (simp add: Let_def)
      apply (rule ccorres_return_CE, simp+)[1]
     apply (simp only: pred_conj_def simp_thms)
     apply wp
    apply (simp add: Collect_const_mem)
    apply vcg
   apply (clarsimp simp: Collect_const_mem if_1_0_0
                         word_sle_def)
   apply (clarsimp simp: cap_get_tag_isCap isCap_simps)
  apply (cinit lift: vptr_' cap_')
   apply csymbr
   apply (simp add: ArchVSpace_H.checkValidIPCBuffer_def
                    cap_get_tag_isCap)
   apply csymbr
   apply simp
   apply (rule ccorres_rhs_assoc)+
   apply csymbr
   apply csymbr
   apply (simp add: cap_get_tag_isCap)
   apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
    apply vcg
   apply (rule conseqPre, vcg)
   apply (clarsimp simp: syscall_error_rel_def syscall_error_to_H_cases
                         exception_defs throwError_def return_def
                  split: capability.split arch_capability.split)
   apply (auto simp add: isCap_simps)[1]
  apply simp
  done

lemma slotCapLongRunningDelete_ccorres:
  "ccorres (op = \<circ> from_bool) ret__unsigned_long_' invs'
           (UNIV \<inter> {s. slot_' s = cte_Ptr slot}) []
     (slotCapLongRunningDelete slot) (Call slotCapLongRunningDelete_'proc)"
  apply (cinit lift: slot_')
   apply (simp add: case_Null_If del: Collect_const)
   apply (rule ccorres_pre_getCTE)
   apply (rule ccorres_move_c_guard_cte)
   apply (rule_tac P="cte_wp_at' (op = rv) slot"
                in ccorres_cross_over_guard)
   apply (rule ccorres_symb_exec_r)
     apply (rule ccorres_if_lhs)
      apply (rule ccorres_cond_true_seq)
      apply (rule ccorres_split_throws, rule ccorres_return_C, simp+)
      apply vcg
     apply (rule ccorres_cond_false_seq)
     apply (rule ccorres_rhs_assoc)+
     apply (rule_tac xf'=ret__unsigned_long_' in ccorres_split_nothrow_novcg)
         apply (ctac add: isFinalCapability_ccorres[where slot=slot])
        apply (rule Seq_weak_ceqv)
        apply (rule Cond_ceqv [OF _ ceqv_refl ceqv_refl])
        apply simp
        apply (rule impI, rule sym, rule mem_simps)
       apply (clarsimp simp del: Collect_const)
       apply (rule ccorres_Cond_rhs_Seq)
        apply (rule ccorres_split_throws, rule ccorres_return_C, simp+)
        apply vcg
       apply (simp del: Collect_const)
       apply (rule ccorres_move_c_guard_cte)
       apply (rule_tac P="cte_wp_at' (op = rv) slot"
                  in  ccorres_from_vcg_throws[where P'=UNIV])
       apply (rule allI, rule conseqPre, vcg)
       apply (clarsimp simp: cte_wp_at_ctes_of return_def)
       apply (erule(1) cmap_relationE1 [OF cmap_relation_cte])
       apply (clarsimp simp: typ_heap_simps cap_get_tag_isCap
                             from_bool_0
                      dest!: ccte_relation_ccap_relation)
       apply (simp add: from_bool_def false_def true_def
                 split: bool.split)
       apply (auto simp add: longRunningDelete_def isCap_simps
                 split: capability.split)[1]
      apply simp
      apply (wp hoare_drop_imps isFinalCapability_inv)
     apply (clarsimp simp: Collect_const_mem guard_is_UNIV_def
                           from_bool_0 false_def true_def)
    apply vcg
   apply (rule conseqPre, vcg, clarsimp)
  apply (clarsimp simp: cte_wp_at_ctes_of)
  apply (erule(1) cmap_relationE1 [OF cmap_relation_cte])
  apply (clarsimp simp: typ_heap_simps cap_get_tag_isCap
                        from_bool_def false_def map_comp_Some_iff
                 dest!: ccte_relation_ccap_relation)
  done

(* FIXME: move *)
lemma empty_fail_slotCapLongRunningDelete:
  "empty_fail (slotCapLongRunningDelete slot)"
  by (auto simp: slotCapLongRunningDelete_def Let_def
                 case_Null_If isFinalCapability_def
          split: split_if
         intro!: empty_fail_bind)

definition
  isValidVTableRoot_C :: "cap_C \<Rightarrow> bool"
where
 "isValidVTableRoot_C cap \<equiv> cap_get_tag cap = scast cap_page_directory_cap
             \<and> to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap))"

lemma isValidVTableRoot_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s} Call isValidVTableRoot_'proc
    {s'. ret__unsigned_long_' s' = from_bool (isValidVTableRoot_C (cap_' s))}"
  apply vcg
  apply (clarsimp simp: isValidVTableRoot_C_def if_1_0_0 from_bool_0)
  apply (simp add: from_bool_def to_bool_def false_def split: split_if)
  done

lemma isValidVTableRoot_conv:
  "\<lbrakk> ccap_relation cap cap' \<rbrakk>
      \<Longrightarrow> isValidVTableRoot_C cap' = isValidVTableRoot cap"
  apply (clarsimp simp: isValidVTableRoot_C_def
                        if_1_0_0 from_bool_0 isValidVTableRoot_def
                        ArchVSpace_H.isValidVTableRoot_def)
  apply (case_tac "isArchCap_tag (cap_get_tag cap')")
   apply (clarsimp simp: cap_get_tag_isCap cap_get_tag_isCap_ArchObject)
   apply (case_tac "cap_get_tag cap' = scast cap_page_directory_cap")
    apply (clarsimp split: arch_capability.split simp: isCap_simps)
    apply (clarsimp simp: ccap_relation_def option_map_Some_eq2
                          cap_page_directory_cap_lift cap_to_H_def
                          from_bool_def)
    apply (clarsimp simp: to_bool_def split: split_if)
   apply (clarsimp simp: cap_get_tag_isCap cap_get_tag_isCap_ArchObject)
   apply (simp split: arch_capability.split_asm add: isCap_simps)
  apply (case_tac "cap_get_tag cap' = scast cap_page_directory_cap")
   apply (clarsimp simp: cap_page_directory_cap_def isArchCap_tag_def2)
  apply (clarsimp simp: cap_get_tag_isCap split: capability.split_asm)
  done

lemma updateCapData_spec:
  "\<forall>cap preserve newData. \<Gamma>\<turnstile> \<lbrace>ccap_relation cap \<acute>cap \<and> preserve = to_bool \<acute>preserve \<and> newData = \<acute>newData\<rbrace>
             Call updateCapData_'proc
         \<lbrace>ccap_relation (RetypeDecls_H.updateCapData preserve newData cap) \<acute>ret__struct_cap_C\<rbrace>"
  by (simp add: updateCapData_spec)

lemma if_n_updateCapData_valid_strg:
  "s \<turnstile>' cap \<longrightarrow> s \<turnstile>' (if P then cap else updateCapData prs v cap)"
  by (simp add: valid_updateCapDataI split: split_if)

lemma length_excaps_map:
  "length (excaps_map xcs) = length xcs"
  by (simp add: excaps_map_def)

(* FIXME: move *)
lemma from_bool_all_helper:
  "(\<forall>bool. from_bool bool = val \<longrightarrow> P bool)
      = ((\<exists>bool. from_bool bool = val) \<longrightarrow> P (val \<noteq> 0))"
  by (auto simp: from_bool_0)

lemma thread_control_update_all_or:
  "thread_control_update_all
     = thread_control_update_priority
        || thread_control_update_ipc_buffer
        || thread_control_update_space"
  apply (simp add: thread_control_flag_defs)
  done

lemma getSyscallArg_ccorres_foo':
  "ccorres (\<lambda>a rv. rv = ucast (args ! n)) (\<lambda>x. ucast (ret__unsigned_long_' x))
         (sysargs_rel args buffer and sysargs_rel_n args buffer n)
         (UNIV \<inter> \<lbrace>unat \<acute>i = n\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>) []
    (return ()) (Call getSyscallArg_'proc)"
  apply (insert getSyscallArg_ccorres_foo
          [where args=args and n=n and buffer=buffer])
  apply (clarsimp simp: ccorres_underlying_def)
  apply  (erule (1) my_BallE)
  apply clarsimp
  apply (erule allE, erule allE, erule (1) impE)
  apply (clarsimp simp: return_def unif_rrel_def split: xstate.splits)
  done

lemma scast_mask_8:
  "scast (mask 8 :: sword32) = (mask 8 :: word32)"
  by (clarsimp simp: mask_def)

lemma decodeTCBConfigure_ccorres:
  notes tl_drop_1[simp] scast_mask_8 [simp]
  shows
  "interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
   ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and sch_act_simple
              and (\<lambda>s. ksCurThread s = thread) and ct_active'
              and (excaps_in_mem extraCaps o ctes_of)
              and valid_cap' cp and cte_at' slot and K (isThreadCap cp)
              and ex_nonz_cap_to' (capTCBPtr cp) and tcb_at' (capTCBPtr cp)
              and (\<lambda>s. \<forall>v \<in> set extraCaps.
                             s \<turnstile>' fst v \<and> cte_at' (snd v) s)
              and (\<lambda>s. \<forall>v \<in> set extraCaps.
                             ex_cte_cap_wp_to' isCNodeCap (snd v) s)
              and sysargs_rel args buffer)
       (UNIV
            \<inter> {s. ccap_relation cp (cap_' s)}
            \<inter> {s. unat (length_' s) = length args}
            \<inter> {s. slot_' s = cte_Ptr slot}
            \<inter> {s. rootCaps_' s = extraCaps'}
            \<inter> {s. buffer_' s = option_to_ptr buffer}) []
     (decodeTCBConfigure args cp slot extraCaps
            >>= invocationCatch thread isBlocking isCall InvokeTCB)
     (Call decodeTCBConfigure_'proc)"
  apply (cinit' lift: cap_' length_' slot_' rootCaps_' buffer_' simp: decodeTCBConfigure_def)
   apply csymbr
   apply (clarsimp cong: StateSpace.state.fold_congs globals.fold_congs
               simp del: Collect_const
               simp add: interpret_excaps_test_null2 excaps_map_Nil)
   apply (rule ccorres_Cond_rhs_Seq)
    apply (rule ccorres_cond_true_seq | simp)+
    apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
     apply vcg
    apply (rule conseqPre, vcg)
    apply (clarsimp simp: if_1_0_0 word_less_nat_alt)
    apply (clarsimp split: list.split
                     simp: throwError_def invocationCatch_def fst_return
                           intr_and_se_rel_def
                           Collect_const_mem syscall_error_rel_def
                           exception_defs syscall_error_to_H_cases)
   apply (rule ccorres_Guard_Seq)+
   apply csymbr
   apply (rule ccorres_Cond_rhs_Seq)
    apply (rule ccorres_cond_true_seq | simp)+
    apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
     apply vcg
    apply (rule conseqPre, vcg)
    apply (clarsimp simp: if_1_0_0 word_less_nat_alt)
    apply (clarsimp split: list.split
                     simp: throwError_def invocationCatch_def fst_return
                           intr_and_se_rel_def
                           Collect_const_mem syscall_error_rel_def
                           exception_defs syscall_error_to_H_cases)
   apply (rule ccorres_Guard_Seq)+
   apply csymbr
   apply (rule ccorres_Cond_rhs_Seq)
    apply (rule ccorres_cond_true_seq | simp)+
    apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
     apply vcg
    apply (rule conseqPre, vcg)
    apply (clarsimp simp: if_1_0_0 word_less_nat_alt)
    apply (clarsimp split: list.split
                     simp: throwError_def invocationCatch_def fst_return
                           intr_and_se_rel_def excaps_map_def
                           Collect_const_mem syscall_error_rel_def
                           exception_defs syscall_error_to_H_cases)
   apply (rule ccorres_Guard_Seq)+
   apply csymbr
   apply (rule ccorres_Cond_rhs_Seq)
    apply (rule ccorres_cond_true_seq | simp)+
    apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
     apply vcg
    apply (rule conseqPre, vcg)
    apply (clarsimp simp: if_1_0_0 word_less_nat_alt)
    apply (clarsimp split: list.split
                     simp: throwError_def invocationCatch_def fst_return
                           intr_and_se_rel_def excaps_map_def
                           Collect_const_mem syscall_error_rel_def
                           exception_defs syscall_error_to_H_cases)
   apply (simp add: if_1_0_0 word_less_nat_alt linorder_not_less
               del: Collect_const)
   apply (rename_tac length' cap')
   apply (subgoal_tac "length extraCaps \<ge> 3")
    prefer 2
    apply (clarsimp simp: idButNot_def interpret_excaps_test_null
                          excaps_map_def neq_Nil_conv)
   apply (thin_tac "P \<longrightarrow> index exc n \<noteq> NULL" for P exc n)+
   apply (rule_tac P="\<lambda>a. ccorres rvr xf P P' hs a c" for rvr xf P P' hs c in ssubst,
          rule bind_cong [OF _ refl], rule list_case_helper, clarsimp)+
   apply (simp add: hd_drop_conv_nth2 del: Collect_const)
   apply (rule ccorres_add_return,
          ctac add: getSyscallArg_ccorres_foo[where args=args and n=0 and buffer=buffer])
     apply (rule ccorres_add_return,
            ctac add: getSyscallArg_ccorres_foo'[where args=args and n=1 and buffer=buffer])
       apply (rule ccorres_add_return,
              ctac add: getSyscallArg_ccorres_foo[where args=args and n=2 and buffer=buffer])
         apply (rule ccorres_add_return,
                ctac add: getSyscallArg_ccorres_foo[where args=args and n=3 and buffer=buffer])
           apply (rule ccorres_add_return,
                  ctac add: getSyscallArg_ccorres_foo[where args=args and n=4 and buffer=buffer])
             apply (rule ccorres_Guard_Seq)+
             apply csymbr
             apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=0])
             apply (rule ccorres_move_c_guard_cte)
             apply ctac
               apply (rule ccorres_assert2)
               apply (rule ccorres_Guard_Seq)+
               apply csymbr
               apply (rule ccorres_move_c_guard_cte)
               apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=1])
               apply ctac
                 apply (rule ccorres_assert2)
                 apply (rule ccorres_Guard_Seq)+
                 apply csymbr
                 apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=2])
                 apply (rule ccorres_move_c_guard_cte)
                 apply ctac
                   apply (rule ccorres_assert2)
                   apply (rule ccorres_Guard_Seq)+
                   apply csymbr
                   apply (rule ccorres_Guard_Seq)
                   apply (simp add: decodeSetPriority_def bindE_assoc getCurThread_def
                               del: Collect_const,
                          simp add: liftE_bindE bind_assoc del: Collect_const)
                   apply (rule ccorres_symb_exec_l3 [OF _ _ _ empty_fail_gets])
                     apply (rule ccorres_symb_exec_l3 [OF _ _ _ empty_fail_threadGet])
                       apply (simp add: invocationCatch_use_injection_handler
                                        injection_bindE [OF refl refl]
                                        injection_handler_If injection_handler_returnOk
                                        whenE_def bindE_assoc if_to_top_of_bindE
                                        ccorres_seq_cond_raise
                                   del: Collect_const cong: if_cong)
                       apply (rule_tac R="obj_at' (\<lambda>t. tcbPriority t = rva) rv
                                             and (\<lambda>s. ksCurThread s = thread \<and> rv = thread)"
                                     in ccorres_cond2)
                         apply (clarsimp simp: rf_sr_ksCurThread)
                         apply (drule obj_at_ko_at', clarsimp+)
                         apply (erule cmap_relationE1 [OF cmap_relation_tcb], erule ko_at_projectKO_opt)
                         apply (clarsimp simp: typ_heap_simps ctcb_relation_def)
                         apply (simp add: word32_FF_is_mask ucast_ucast_mask8)
                         apply (drule sym, simp, fastforce simp: unat_ucast_8_32 word_less_nat_alt)
                        apply (simp add: injection_handler_throwError)
                        apply (rule syscall_error_throwError_ccorres_n)
                        apply (simp add: syscall_error_to_H_cases)
                       apply (simp add: decodeSetIPCBuffer_def
                                        split_def
                                        injection_handler_If injection_handler_returnOk
                                        injection_bindE [OF refl refl] bindE_assoc
                                   del: Collect_const cong: if_cong)
                       apply (rule_tac xf'="\<lambda>s. (bufferCap_' s, bufferSlot_' s)"
                                    and r'="\<lambda>v (cp', sl'). case v of None \<Rightarrow> args ! 4 = 0 \<and> sl' = cte_Ptr 0
                                                   | Some (cp, sl) \<Rightarrow> ccap_relation cp cp'
                                                            \<and> args ! 4 \<noteq> 0 \<and> sl' = cte_Ptr sl"
                                  in ccorres_splitE)
                           apply (rule ccorres_cond2[where R=\<top>])
                             apply (clarsimp simp add: Collect_const_mem numeral_eqs)
                            apply (rule_tac P="\<lambda>s. args ! 4 = 0" in ccorres_from_vcg[where P'=UNIV])
                            apply (rule allI, rule conseqPre, vcg)
                            apply (clarsimp simp: returnOk_def return_def)
                           apply (rule ccorres_rhs_assoc)+
                           apply csymbr
                           apply (rule ccorres_split_nothrowE)
                                apply (simp add: numeral_eqs)
                                apply (ctac add: ccorres_injection_handler_csum1[OF deriveCap_ccorres])
                               apply ceqv
                              apply simp
                              apply csymbr
                              apply (rule ccorres_split_nothrowE)
                                   apply (ctac add: ccorres_injection_handler_csum1[OF checkValidIPCBuffer_ccorres])
                                  apply ceqv
                                 apply (rule_tac P'="{s. bufferCap_' s = deriveCap_ret_C.cap_C rv'
                                                          \<and> bufferSlot_' s = cte_Ptr (snd (extraCaps ! 2))}"
                                              and P="\<lambda>s. args ! 4 \<noteq> 0"
                                             in ccorres_from_vcg)
                                 apply (rule allI, rule conseqPre, vcg)
                                 apply (clarsimp simp: returnOk_def return_def numeral_eqs)
                                apply (rule_tac P'="{s. err' = errstate s}"
                                            in ccorres_from_vcg_throws[where P=\<top>])
                                apply (rule allI, rule conseqPre, vcg)
                                apply (clarsimp simp: throwError_def return_def
                                                      syscall_error_rel_def
                                                      intr_and_se_rel_def)
                               apply wp
                              apply simp
                              apply (vcg exspec=checkValidIPCBuffer_modifies)
                             apply simp
                             apply (rule_tac P'="{s. err' = errstate s}"
                                        in  ccorres_from_vcg_split_throws[where P=\<top>])
                              apply vcg
                             apply (rule conseqPre, vcg)
                             apply (clarsimp simp: throwError_def return_def
                                                   intr_and_se_rel_def syscall_error_rel_def)
                            apply simp
                            apply (wp injection_wp_E [OF refl])
                           apply (simp add: all_ex_eq_helper Collect_const_mem numeral_eqs)
                           apply (vcg exspec=deriveCap_modifies)
                          apply (rule ceqv_tuple2, ceqv, ceqv)
                         apply (rule_tac P="P (fst rv') (snd rv')"
                                    and P'="P' (fst rv') (snd rv')" for P P' in ccorres_inst)
                         apply (clarsimp simp del: Collect_const)
                         apply csymbr
                         apply (rule ccorres_Guard_Seq)+
                         apply (simp add: decodeSetSpace_def injection_bindE[OF refl]
                                          split_def del: Collect_const)
                         apply (simp add: injection_liftE[OF refl] bindE_assoc
                                          liftM_def getThreadCSpaceRoot
                                          getThreadVSpaceRoot del: Collect_const)
                         apply (simp add: liftE_bindE del: Collect_const)
                         apply (ctac add: slotCapLongRunningDelete_ccorres)
                           apply csymbr
                           apply (clarsimp simp add: if_1_0_0 from_bool_0
                                           simp del: Collect_const)
                           apply (rule ccorres_Cond_rhs_Seq)
                            apply (rule ccorres_symb_exec_l3
                                      [OF _ _ _ empty_fail_slotCapLongRunningDelete])
                              apply (simp add: unlessE_def injection_handler_throwError
                                         cong: StateSpace.state.fold_congs globals.fold_congs)
                              apply (rule ccorres_cond_true_seq)
                              apply (rule syscall_error_throwError_ccorres_n)
                              apply (simp add: syscall_error_to_H_cases)
                             apply wp
                           apply (rule ccorres_rhs_assoc)+
                           apply csymbr
                           apply (rule ccorres_Guard_Seq)+
                           apply (ctac add: slotCapLongRunningDelete_ccorres)
                             apply csymbr
                             apply (clarsimp simp add: if_1_0_0 from_bool_0
                                             simp del: Collect_const)
                             apply (rule ccorres_Cond_rhs_Seq)
                              apply (simp add: unlessE_def injection_handler_throwError
                                         cong: StateSpace.state.fold_congs globals.fold_congs)
                              apply (rule syscall_error_throwError_ccorres_n)
                              apply (simp add: syscall_error_to_H_cases)
                             apply (simp add: unlessE_def injection_handler_returnOk
                                         del: Collect_const)
                             apply (rule ccorres_add_return,
                                    rule_tac r'="\<lambda>rv rv'. ccap_relation (if args ! 2 = 0 then fst (hd extraCaps)
                                                       else updateCapData False (args ! 2) (fst (hd extraCaps))) rv'"
                                         and xf'="cRootCap_'" in ccorres_split_nothrow)
                                 apply (rule_tac P'="{s. cRootCap = cRootCap_' s}"
                                             in ccorres_from_vcg[where P=\<top>])
                                 apply (rule allI, rule conseqPre, vcg)
                                 apply (subgoal_tac "extraCaps \<noteq> []")
                                  apply (clarsimp simp: returnOk_def return_def hd_conv_nth false_def)
                                  apply fastforce
                                 apply clarsimp
                                apply ceqv
                               apply (ctac add: ccorres_injection_handler_csum1
                                                  [OF deriveCap_ccorres])
                                  apply (simp add: Collect_False del: Collect_const)
                                  apply (csymbr, csymbr)
                                  apply (simp add: cap_get_tag_isCap cnode_cap_case_if
                                              del: Collect_const)
                                  apply (rule ccorres_Cond_rhs_Seq)
                                   apply (simp add: injection_handler_throwError
                                              cong: StateSpace.state.fold_congs globals.fold_congs)
                                   apply (rule syscall_error_throwError_ccorres_n)
                                   apply (simp add: syscall_error_to_H_cases)
                                  apply (simp add: injection_handler_returnOk del: Collect_const)
                                  apply (rule ccorres_add_return,
                                         rule_tac r'="\<lambda>rv rv'. ccap_relation (if args ! 3 = 0 then fst (extraCaps ! Suc 0)
                                                            else updateCapData False (args ! 3) (fst (extraCaps ! Suc 0))) rv'"
                                              and xf'="vRootCap_'" in ccorres_split_nothrow)
                                      apply (rule_tac P'="{s. vRootCap = vRootCap_' s}"
                                             in ccorres_from_vcg[where P=\<top>])
                                      apply (rule allI, rule conseqPre, vcg)
                                      apply (clarsimp simp: returnOk_def return_def
                                                            hd_drop_conv_nth2 false_def)
                                      apply fastforce
                                     apply ceqv
                                    apply (ctac add: ccorres_injection_handler_csum1
                                                        [OF deriveCap_ccorres])
                                       apply (simp add: Collect_False del: Collect_const)
                                       apply csymbr
                                       apply csymbr
                                       apply (simp add: from_bool_0 isValidVTableRoot_conv del: Collect_const)
                                       apply (rule ccorres_Cond_rhs_Seq)
                                        apply (simp add: injection_handler_throwError
                                                   cong: StateSpace.state.fold_congs globals.fold_congs)
                                        apply (rule syscall_error_throwError_ccorres_n)
                                        apply (simp add: syscall_error_to_H_cases)
                                       apply (simp add: injection_handler_returnOk ccorres_invocationCatch_Inr
                                                        performInvocation_def)
                                       apply (ctac add: setThreadState_ccorres)
                                         apply csymbr
                                         apply (ctac(no_vcg) add: invokeTCB_ThreadControl_ccorres)
                                           apply (simp, rule ccorres_alternative2)
                                           apply (rule ccorres_return_CE, simp+)
                                          apply (rule ccorres_return_C_errorE, simp+)[1]
                                         apply wp
                                        apply (simp add: o_def)
                                        apply (wp sts_invs_minor' hoare_case_option_wp)
                                       apply (simp add: Collect_const_mem cintr_def intr_and_se_rel_def
                                                        exception_defs cong: option.case_cong)
                                       apply (vcg exspec=setThreadState_modifies)
                                      apply simp
                                      apply (rule ccorres_split_throws, rule ccorres_return_C_errorE, simp+)
                                      apply vcg
                                     apply simp
                                     apply (wp injection_wp_E[OF refl] hoare_drop_imps)
                                    apply (vcg exspec=deriveCap_modifies)
                                   apply (simp add: pred_conj_def cong: if_cong)
                                   apply wp
                                  apply (simp add: Collect_const_mem)
                                  apply (vcg)
                                 apply simp
                                 apply (rule ccorres_split_throws, rule ccorres_return_C_errorE, simp+)
                                 apply vcg
                                apply (simp cong: if_cong)
                                apply (wp injection_wp_E[OF refl] hoare_drop_imps)
                               apply (simp add: Collect_const_mem intr_and_se_rel_def
                                                syscall_error_rel_def exception_defs
                                          cong: option.case_cong sum.case_cong)
                               apply (simp add: all_ex_eq_helper numeral_eqs)
                               apply (vcg exspec=deriveCap_modifies)
                              apply (simp cong: if_cong)
                              apply wp
                             apply (simp add: Collect_const_mem del: Collect_const)
                             apply vcg
                            apply (simp cong: if_cong)
                            apply (wp hoare_drop_imps)
                           apply (simp add: Collect_const_mem all_ex_eq_helper
                                      cong: option.case_cong)
                           apply (vcg exspec=slotCapLongRunningDelete_modifies)
                          apply (simp cong: if_cong)
                          apply (wp hoare_drop_imps)
                         apply (simp add: Collect_const_mem)
                         apply (vcg exspec=slotCapLongRunningDelete_modifies)
                        apply (simp add: pred_conj_def cong: if_cong)
                        apply (wp injection_wp_E[OF refl] checkValidIPCBuffer_ArchObject_wp)
                        apply simp
                        apply (wp hoare_drop_imps)
                       apply (simp add: Collect_const_mem all_ex_eq_helper)
                       apply (rule_tac P="{s. cRootCap_' s = cRootCap \<and> vRootCap_' s = vRootCap
                                                  \<and> bufferAddr_' s = args ! 4
                                                  \<and> ccap_relation cp cap' \<and> isThreadCap cp
                                                  \<and> is_aligned (capTCBPtr cp) 9
                                                  \<and> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr thread}"
                                   in conseqPre)
                        apply (simp add: cong: option.case_cong)
                        apply (vcg exspec=deriveCap_modifies exspec=checkValidIPCBuffer_modifies)
                       apply (clarsimp simp: excaps_map_def Collect_const_mem ccHoarePost_def
                                             numeral_eqs cong: option.case_cong)
                       apply (frule interpret_excaps_eq[rule_format, where n=0], clarsimp)
                       apply (frule interpret_excaps_eq[rule_format, where n=1], clarsimp)
                       apply (frule interpret_excaps_eq[rule_format, where n=2], clarsimp)
                       apply (clarsimp simp: mask_def[where n=4] ccap_rights_relation_def
                                             rightsFromWord_wordFromRights
                                             capTCBPtr_eq ptr_val_tcb_ptr_mask2[unfolded mask_def, simplified]
                                             tcb_cnode_index_defs size_of_def
                                             option_to_0_def rf_sr_ksCurThread
                                             "StrictC'_thread_state_defs" mask_eq_iff_w2p word_size
                                             thread_control_update_all_or
                                             from_bool_all_helper all_ex_eq_helper)
                       apply (subgoal_tac "args \<noteq> [] \<and> extraCaps \<noteq> []")
                        apply (simp add: word_sle_def cap_get_tag_isCap numeral_eqs
                                         hd_conv_nth hd_drop_conv_nth2 ucast_ucast_mask8
                                         word32_FF_is_mask split_def
                                         thread_control_update_priority_def
                                         thread_control_update_space_def
                                         thread_control_update_ipc_buffer_def
                                         cast_simps)
                        apply (auto split: option.split elim!: inl_inrE,
                               fastforce?)[1]
                       apply fastforce
                      apply wp[1]
                     apply (simp add: numeral_eqs cong: if_cong)
                     apply (wp threadGet_obj_at2)
                     apply (wp hoare_drop_imps)[1]
                    apply wp[1]
                   apply (simp cong: if_cong)
                   apply wp[1]
                  apply (strengthen if_n_updateCapData_valid_strg)
                  apply (wp hoare_drop_imps)
                 apply (clarsimp simp: Collect_const_mem all_ex_eq_helper
                                 cong: option.case_cong)
                 apply vcg
                apply simp
                apply (strengthen if_n_updateCapData_valid_strg)
                apply (wp hoare_drop_imps)
               apply (simp add: Collect_const_mem all_ex_eq_helper)
               apply vcg
              apply simp
              apply (wp hoare_drop_imps)
             apply vcg
            apply wp
           apply (vcg exspec=getSyscallArg_modifies)
          apply wp
         apply (vcg exspec=getSyscallArg_modifies)
        apply wp
        apply simp
       apply (vcg exspec=getSyscallArg_modifies)
      apply wp
     apply (vcg exspec=getSyscallArg_modifies)
    apply wp
   apply (vcg exspec=getSyscallArg_modifies)
  apply (clarsimp simp: Collect_const_mem all_ex_eq_helper
                        if_1_0_0)
  apply (rule conjI)
   apply (clarsimp simp: idButNot_def interpret_excaps_test_null
                         excaps_map_def neq_Nil_conv)
   apply (clarsimp simp: sysargs_rel_to_n word_less_nat_alt)
   apply (frule invs_mdb')
   apply (simp add: maxPriority_def numPriorities_def)
   apply (fold max_word_def[where 'a=8, simplified])
   apply (auto simp: ct_in_state'_def valid_mdb'_def valid_mdb_ctes_def
                     cte_wp_at_ctes_of no_0_def valid_tcb_state'_def
              elim!: st_tcb'_weakenE
              dest!: st_tcb_at_idle_thread' interpret_excaps_eq)[1]
  apply (clarsimp simp: idButNot_def interpret_excaps_test_null
                        excaps_map_def neq_Nil_conv word_sle_def word_sless_def)
  apply (frule interpret_excaps_eq[rule_format, where n=0], simp)
  apply (frule interpret_excaps_eq[rule_format, where n=1], simp)
  apply (frule interpret_excaps_eq[rule_format, where n=2], simp)
  apply (clarsimp simp: mask_def[where n=4] ccap_rights_relation_def
                        rightsFromWord_wordFromRights
                        capTCBPtr_eq tcb_ptr_to_ctcb_ptr_mask
                        tcb_cnode_index_defs size_of_def
                        option_to_0_def rf_sr_ksCurThread
                        "StrictC'_thread_state_defs" mask_eq_iff_w2p word_size
                        thread_control_update_all_or
                        from_bool_all_helper)
  apply (frule(1) tcb_at_h_t_valid [OF tcb_at_invs'])
  apply (clarsimp simp: typ_heap_simps numeral_eqs)
  apply (clarsimp simp: isCap_simps valid_cap'_def capAligned_def
                        objBits_simps)
  done

lemma decodeSetPriority_ccorres:
  notes scast_mask_8 [simp]
  shows
  "ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and (\<lambda>s. ksCurThread s = thread)
              and ct_active' and sch_act_simple
              and (\<lambda>s. \<forall>rf \<in> zobj_refs' cp. ex_nonz_cap_to' rf s)
              and valid_cap' cp and K (isThreadCap cp)
              and sysargs_rel args buffer)
       (UNIV
            \<inter> {s. ccap_relation cp (cap_' s)}
            \<inter> {s. unat (length_' s) = length args}
            \<inter> {s. buffer_' s = option_to_ptr buffer}) []
     (decodeSetPriority args cp
            >>= invocationCatch thread isBlocking isCall InvokeTCB)
     (Call decodeSetPriority_'proc)"
  apply (cinit' lift: cap_' length_' buffer_' simp: decodeSetPriority_def)
   apply wpc
    apply (simp add: throwError_bind invocationCatch_def)
    apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
     apply vcg
    apply (rule conseqPre, vcg)
    apply (clarsimp simp: throwError_def return_def intr_and_se_rel_def
                          exception_defs syscall_error_rel_def
                          syscall_error_to_H_cases)
   apply (rule ccorres_cond_false_seq)
   apply (simp add: liftE_bindE bind_assoc getCurThread_def)
   apply (rule ccorres_add_return,
          ctac add: getSyscallArg_ccorres_foo'[where args=args and n=0 and buffer=buffer])
     apply (rule ccorres_Guard_Seq)+
     apply csymbr
     apply (rule ccorres_Guard_Seq)
     apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_gets])
       apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_threadGet])
         apply (simp add: bindE_bind_linearise whenE_def if_to_top_of_bind
                          throwError_bind returnOk_bind lift_def
                    cong: if_cong)
         apply (rule_tac Q="\<lambda>s. rva = ksCurThread s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = rvb) rva s"
                     and Q'=\<top> in ccorres_if_cond_throws)
            apply (clarsimp simp add: Collect_const_mem)
            apply (drule obj_at_ko_at', clarsimp)
            apply (frule rf_sr_ksCurThread)
            apply (erule cmap_relationE1 [OF cmap_relation_tcb], erule ko_at_projectKO_opt)
            apply (clarsimp simp: typ_heap_simps ctcb_relation_def)
            apply (simp add: ucast_ucast_mask8 word32_FF_is_mask)
            apply (drule sym, simp, fastforce simp: unat_ucast_8_32 word_less_nat_alt)
           apply (simp add: invocationCatch_def
                      cong: StateSpace.state.fold_congs globals.fold_congs)
           apply (rule syscall_error_throwError_ccorres_n)
           apply (simp add: syscall_error_to_H_cases)
          apply (simp add: ccorres_invocationCatch_Inr performInvocation_def)
          apply (ctac add: setThreadState_ccorres)
            apply csymbr
            apply csymbr
            apply csymbr
            apply csymbr
            apply (ctac(no_vcg) add: invokeTCB_ThreadControl_ccorres)
              apply simp
              apply (rule ccorres_alternative2)
              apply (rule ccorres_return_CE, simp+)[1]
             apply (rule ccorres_return_C_errorE, simp+)[1]
            apply wp
           apply simp
           apply (wp sts_invs_minor')
          apply (vcg exspec=setThreadState_modifies)
         apply vcg
        apply wp
       apply (wp threadGet_wp)[2]
     apply simp
     apply wp
   apply (vcg exspec=getSyscallArg_modifies)
  apply (clarsimp simp: Collect_const_mem intr_and_se_rel_def
                        syscall_error_rel_def syscall_error_to_H_cases
                        exception_defs)
  apply (rule conjI)
   apply (clarsimp simp: ct_in_state'_def st_tcb_at_tcb_at'
                         valid_cap'_def isCap_simps)
   apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def)
   apply (simp add: maxPriority_def numPriorities_def)
   apply (fold max_word_def[where 'a=8, simplified])
   apply (auto simp: valid_tcb_state'_def
              elim!: obj_at'_weakenE st_tcb'_weakenE
              dest!: st_tcb_at_idle_thread')[1]
  apply (simp add: "StrictC'_thread_state_defs" mask_eq_iff_w2p word_size
                   option_to_0_def)
  apply (frule rf_sr_ksCurThread)
  apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
  apply (clarsimp simp: valid_cap'_def capAligned_def)
  apply (intro conjI impI allI)
      apply (clarsimp simp: unat_eq_0)
     apply (clarsimp simp: word32_FF_is_mask ucast_ucast_mask)
    apply (thin_tac "tcb_at' p s" for p s)+
    apply (clarsimp simp: ct_in_state'_def st_tcb_at'_def)
    apply (drule obj_at_ko_at', clarsimp)
    apply (erule cmap_relationE1 [OF cmap_relation_tcb], erule ko_at_projectKO_opt)
    apply (fastforce intro: typ_heap_simps)
   apply (simp add: word_sle_def)
  apply clarsimp
  done

lemma decodeSetIPCBuffer_ccorres:
  "interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
   ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple
              and valid_cap' cp and cte_at' slot and K (isThreadCap cp)
              and (excaps_in_mem extraCaps o ctes_of)
              and (\<lambda>s. \<forall>rf \<in> zobj_refs' cp. ex_nonz_cap_to' rf s)
              and (\<lambda>s. \<forall>v \<in> set extraCaps.
                             s \<turnstile>' fst v \<and> cte_at' (snd v) s)
              and (\<lambda>s. \<forall>v \<in> set extraCaps.
                             ex_cte_cap_wp_to' isCNodeCap (snd v) s)
              and sysargs_rel args buffer)
       (UNIV
            \<inter> {s. ccap_relation cp (cap_' s)}
            \<inter> {s. unat (length_' s) = length args}
            \<inter> {s. slot_' s = cte_Ptr slot}
            \<inter> {s. extraCaps_' s = extraCaps'}
            \<inter> {s. buffer_' s = option_to_ptr buffer}) []
     (decodeSetIPCBuffer args cp slot extraCaps
            >>= invocationCatch thread isBlocking isCall InvokeTCB)
     (Call decodeSetIPCBuffer_'proc)"
  apply (cinit' lift: cap_' length_' slot_' extraCaps_' buffer_'
                simp: decodeSetIPCBuffer_def)
   apply wpc
    apply (simp add: unat_eq_0)
    apply csymbr
    apply simp
    apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
     apply vcg
    apply (rule conseqPre, vcg)
    apply (simp add: throwError_bind invocationCatch_def)
    apply (clarsimp simp: throwError_def return_def
                          intr_and_se_rel_def exception_defs
                          syscall_error_rel_def syscall_error_to_H_cases)
   apply csymbr
   apply (rule ccorres_cond_false_seq)
   apply (rule ccorres_Guard_Seq)+
   apply csymbr
   apply (simp add: interpret_excaps_test_null excaps_map_Nil if_1_0_0
               del: Collect_const)
   apply wpc
    apply (simp add: throwError_bind invocationCatch_def
               cong: StateSpace.state.fold_congs globals.fold_congs)
    apply (rule syscall_error_throwError_ccorres_n)
    apply (simp add: syscall_error_to_H_cases)
   apply (rule ccorres_cond_false_seq)
   apply (simp add: split_def
               del: Collect_const)
   apply (rule ccorres_add_return,
          ctac add: getSyscallArg_ccorres_foo [where args=args and n=0 and buffer=buffer])
     apply (rule ccorres_Guard_Seq)+
     apply csymbr
     apply (rule ccorres_move_c_guard_cte)
     apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=0])
     apply ctac
       apply (rule ccorres_assert2)
       apply (rule ccorres_Cond_rhs_Seq)
        apply (simp add: returnOk_bind ccorres_invocationCatch_Inr performInvocation_def)
        apply csymbr
        apply (ctac add: setThreadState_ccorres)
          apply csymbr
          apply csymbr
          apply csymbr
          apply (ctac add: invokeTCB_ThreadControl_ccorres)
             apply simp
             apply (rule ccorres_alternative2)
             apply (rule ccorres_return_CE, simp+)[1]
            apply (rule ccorres_return_C_errorE, simp+)[1]
           apply wp
          apply (vcg exspec=invokeTCB_ThreadControl_modifies)
         apply simp
         apply (wp sts_invs_minor')
        apply (vcg exspec=setThreadState_modifies)
       apply (simp add: bindE_assoc del: Collect_const)
       apply (rule ccorres_rhs_assoc)+
       apply (csymbr, csymbr)
       apply (simp add: bindE_bind_linearise)
       apply (rule ccorres_split_nothrow_case_sum)
            apply (ctac add: deriveCap_ccorres)
           apply ceqv
          apply (simp add: Collect_False del: Collect_const)
          apply csymbr
          apply (rule ccorres_split_nothrow_case_sum)
               apply (ctac add: checkValidIPCBuffer_ccorres)
              apply ceqv
             apply (simp add: Collect_False returnOk_bind
                              ccorres_invocationCatch_Inr
                         del: Collect_const)
             apply (ctac add: setThreadState_ccorres)
               apply (simp add: performInvocation_def)
               apply (csymbr, csymbr, csymbr)
               apply (ctac add: invokeTCB_ThreadControl_ccorres)
                  apply simp
                  apply (rule ccorres_alternative2)
                  apply (rule ccorres_return_CE, simp+)[1]
                 apply (rule ccorres_return_C_errorE, simp+)[1]
                apply wp
               apply (vcg exspec=invokeTCB_ThreadControl_modifies)
              apply simp
              apply (wp sts_invs_minor')
             apply (simp add: Collect_const_mem cintr_def intr_and_se_rel_def)
             apply (vcg exspec=setThreadState_modifies)
            apply (simp add: invocationCatch_def)
            apply (rule ccorres_split_throws, rule ccorres_return_C_errorE, simp+)
            apply vcg
           apply simp
           apply (wp checkValidIPCBuffer_ArchObject_wp)
          apply (simp add: intr_and_se_rel_def syscall_error_rel_def
                           exception_defs)
          apply (vcg exspec=checkValidIPCBuffer_modifies)
         apply (simp add: invocationCatch_def)
         apply (rule ccorres_split_throws)
          apply (rule ccorres_return_C_errorE, simp+)[1]
         apply vcg
        apply simp
        apply (wp hoare_drop_imps)
       apply (simp add: Collect_const_mem)
       apply (vcg exspec=deriveCap_modifies)
      apply simp
      apply (wp_once hoare_drop_imps)
      apply wp
     apply simp
     apply vcg
    apply wp
   apply simp
   apply (vcg exspec=getSyscallArg_modifies)
  apply (clarsimp simp: Collect_const_mem if_1_0_0 ct_in_state'_def
                        st_tcb_at_tcb_at' cintr_def intr_and_se_rel_def
                        exception_defs syscall_error_rel_def)
  apply (rule conjI)
   apply (clarsimp simp: excaps_in_mem_def slotcap_in_mem_def)
   apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def)
   apply (frule invs_mdb')
   apply (auto simp: isCap_simps valid_cap'_def valid_mdb'_def valid_tcb_state'_def
                     valid_mdb_ctes_def no_0_def excaps_map_def
               elim: st_tcb'_weakenE dest!: st_tcb_at_idle_thread'
              dest!: interpret_excaps_eq)[1]
  apply (clarsimp simp: option_to_0_def rf_sr_ksCurThread word_sless_def
            word_sle_def ThreadState_Restart_def mask_def)
  apply (rule conjI[rotated], clarsimp+)
  apply (drule interpret_excaps_eq[rule_format, where n=0], simp add: excaps_map_Nil)
  apply (simp add: mask_def "StrictC'_thread_state_defs" excaps_map_def)
  apply (clarsimp simp: ccap_rights_relation_def rightsFromWord_wordFromRights
                        cap_get_tag_isCap)
  apply (frule cap_get_tag_to_H, subst cap_get_tag_isCap, assumption, assumption)
  apply clarsimp
  done

lemma decodeSetSpace_ccorres:
  notes tl_drop_1[simp] scast_mask_8 [simp]
  shows
  "interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
   ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple
              and valid_cap' cp and cte_at' slot and K (isThreadCap cp)
              and tcb_at' (capTCBPtr cp)
              and (\<lambda>s. \<forall>rf \<in> zobj_refs' cp. ex_nonz_cap_to' rf s)
              and (excaps_in_mem extraCaps o ctes_of)
              and (\<lambda>s. \<forall>v \<in> set extraCaps.
                             s \<turnstile>' fst v \<and> cte_at' (snd v) s)
              and (\<lambda>s. \<forall>v \<in> set extraCaps.
                             ex_cte_cap_wp_to' isCNodeCap (snd v) s)
              and sysargs_rel args buffer)
       (UNIV
            \<inter> {s. ccap_relation cp (cap_' s)}
            \<inter> {s. unat (length_' s) = length args}
            \<inter> {s. slot_' s = cte_Ptr slot}
            \<inter> {s. extraCaps_' s = extraCaps'}
            \<inter> {s. buffer_' s = option_to_ptr buffer}) []
     (decodeSetSpace args cp slot extraCaps
            >>= invocationCatch thread isBlocking isCall InvokeTCB)
     (Call decodeSetSpace_'proc)"
  apply (cinit' lift: cap_' length_' slot_' extraCaps_' buffer_'
                simp: decodeSetSpace_def)
   apply csymbr
   apply (rule ccorres_Cond_rhs_Seq)
    apply (simp add: if_1_0_0)
    apply (rule ccorres_cond_true_seq | simp)+
    apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
     apply vcg
    apply (rule conseqPre, vcg)
    apply (subgoal_tac "unat length < 3")
     apply (clarsimp simp: throwError_def invocationCatch_def fst_return
                           intr_and_se_rel_def syscall_error_rel_def
                           syscall_error_to_H_cases exception_defs
                           subset_iff
                    split: list.split)
    apply unat_arith
   apply (rule ccorres_Guard_Seq)+
   apply csymbr
   apply (rule ccorres_Cond_rhs_Seq)
    apply (simp add: if_1_0_0 interpret_excaps_test_null excaps_map_Nil)
    apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
     apply vcg
    apply (rule conseqPre, vcg)
    apply clarsimp
    apply (clarsimp simp: throwError_def invocationCatch_def fst_return
                          intr_and_se_rel_def syscall_error_rel_def
                          syscall_error_to_H_cases exception_defs
                   split: list.split)
   apply (rule ccorres_Guard_Seq)+
   apply csymbr
   apply (simp add: if_1_0_0 interpret_excaps_test_null del: Collect_const)
   apply (rule_tac P="\<lambda>c. ccorres rvr xf P P' hs a (Cond c c1 c2 ;; c3)" for rvr xf P P' hs a c1 c2 c3 in ssubst)
    apply (rule Collect_cong)
    apply (rule interpret_excaps_test_null)
     apply (clarsimp simp: neq_Nil_conv)
    apply simp
   apply (rule ccorres_Cond_rhs_Seq)
    apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV])
     apply vcg
    apply (rule conseqPre, vcg)
    apply clarsimp
    apply (clarsimp simp: throwError_def invocationCatch_def fst_return
                          intr_and_se_rel_def syscall_error_rel_def
                          syscall_error_to_H_cases exception_defs
                          excaps_map_def
                   split: list.split)
   apply (clarsimp simp add: linorder_not_less word_le_nat_alt
                             excaps_map_Nil length_excaps_map
                   simp del: Collect_const)
   apply (drule_tac a="Suc 0" in neq_le_trans [OF not_sym])
    apply (clarsimp simp: neq_Nil_conv)
   apply (rule_tac P="\<lambda>a. ccorres rvr xf P P' hs a c" for rvr xf P P' hs c in ssubst,
          rule bind_cong [OF _ refl], rule list_case_helper,
          clarsimp)+
   apply (simp add: hd_drop_conv_nth2 del: Collect_const)
   apply (rule ccorres_add_return,
          ctac add: getSyscallArg_ccorres_foo[where args=args and n=0 and buffer=buffer])
     apply (rule ccorres_add_return,
            ctac add: getSyscallArg_ccorres_foo[where args=args and n=1 and buffer=buffer])
       apply (rule ccorres_add_return,
              ctac add: getSyscallArg_ccorres_foo[where args=args and n=2 and buffer=buffer])
         apply (rule ccorres_Guard_Seq)+
         apply csymbr
         apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=0])
         apply (rule ccorres_move_c_guard_cte)
         apply ctac
           apply (rule ccorres_assert2)
           apply (rule ccorres_Guard_Seq)+
           apply csymbr
           apply (rule getSlotCap_ccorres_fudge_n[where vals=extraCaps and n=1])
           apply (rule ccorres_move_c_guard_cte)
           apply ctac
             apply (rule ccorres_assert2)
             apply csymbr
             apply (rule ccorres_Guard_Seq)+
             apply (simp add: decodeSetSpace_def injection_bindE[OF refl]
                              split_def del: Collect_const)
             apply (simp add: injection_liftE[OF refl] bindE_assoc
                              liftM_def getThreadCSpaceRoot
                              getThreadVSpaceRoot del: Collect_const)
             apply (simp add: liftE_bindE bind_assoc del: Collect_const)
             apply (ctac add: slotCapLongRunningDelete_ccorres)
               apply csymbr
               apply (clarsimp simp add: if_1_0_0 from_bool_0
                               simp del: Collect_const)
               apply (rule ccorres_Cond_rhs_Seq)
                apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_slotCapLongRunningDelete])
                  apply (simp add: unlessE_def throwError_bind invocationCatch_def
                             cong: StateSpace.state.fold_congs globals.fold_congs)
                  apply (rule ccorres_cond_true_seq)
                  apply (rule syscall_error_throwError_ccorres_n)
                  apply (simp add: syscall_error_to_H_cases)
                 apply wp
               apply (rule ccorres_rhs_assoc)+
               apply csymbr
               apply (rule ccorres_Guard_Seq)+
               apply (ctac add: slotCapLongRunningDelete_ccorres)
                 apply csymbr
                 apply (clarsimp simp add: if_1_0_0 from_bool_0
                                 simp del: Collect_const)
                 apply (rule ccorres_Cond_rhs_Seq)
                  apply (simp add: unlessE_def throwError_bind invocationCatch_def
                             cong: StateSpace.state.fold_congs globals.fold_congs)
                  apply (rule syscall_error_throwError_ccorres_n)
                  apply (simp add: syscall_error_to_H_cases)
                 apply (simp add: unlessE_def
                             del: Collect_const)
                 apply (rule ccorres_add_return,
                        rule_tac r'="\<lambda>rv rv'. ccap_relation (if args ! Suc 0 = 0 then fst (hd extraCaps)
                                           else updateCapData False (args ! Suc 0) (fst (hd extraCaps))) rv'"
                             and xf'="cRootCap_'" in ccorres_split_nothrow)
                     apply (rule_tac P'="{s. cRootCap = cRootCap_' s}"
                                 in ccorres_from_vcg[where P=\<top>])
                     apply (rule allI, rule conseqPre, vcg)
                     apply (subgoal_tac "extraCaps \<noteq> []")
                      apply (clarsimp simp: returnOk_def return_def hd_conv_nth false_def)
                      apply fastforce
                     apply clarsimp
                    apply ceqv
                   apply (simp add: invocationCatch_use_injection_handler
                                    injection_bindE [OF refl refl] bindE_assoc
                               del: Collect_const)
                   apply (ctac add: ccorres_injection_handler_csum1
                                              [OF deriveCap_ccorres])
                      apply (simp add: Collect_False del: Collect_const)
                      apply csymbr
                      apply csymbr
                      apply (simp add: cnode_cap_case_if cap_get_tag_isCap dc_def[symmetric]
                                  del: Collect_const)
                      apply (rule ccorres_Cond_rhs_Seq)
                       apply (simp add: injection_handler_throwError
                                  cong: StateSpace.state.fold_congs globals.fold_congs)
                       apply (rule syscall_error_throwError_ccorres_n)
                       apply (simp add: syscall_error_to_H_cases)
                      apply (simp add: injection_handler_returnOk del: Collect_const)
                      apply (rule ccorres_add_return,
                             rule_tac r'="\<lambda>rv rv'. ccap_relation (if args ! 2 = 0 then fst (extraCaps ! Suc 0)
                                                else updateCapData False (args ! 2) (fst (extraCaps ! Suc 0))) rv'"
                                  and xf'="vRootCap_'" in ccorres_split_nothrow)
                           apply (rule_tac P'="{s. vRootCap = vRootCap_' s}"
                                  in ccorres_from_vcg[where P=\<top>])
                           apply (rule allI, rule conseqPre, vcg)
                           apply (clarsimp simp: returnOk_def return_def
                                                 hd_drop_conv_nth2 false_def)
                           apply fastforce
                          apply ceqv
                         apply (ctac add: ccorres_injection_handler_csum1
                                             [OF deriveCap_ccorres])
                            apply (simp add: Collect_False del: Collect_const)
                            apply csymbr
                            apply csymbr
                            apply (simp add: from_bool_0 isValidVTableRoot_conv del: Collect_const)
                            apply (rule ccorres_Cond_rhs_Seq)
                             apply (simp add: injection_handler_throwError
                                        cong: StateSpace.state.fold_congs globals.fold_congs)
                             apply (rule syscall_error_throwError_ccorres_n)
                             apply (simp add: syscall_error_to_H_cases)
                            apply (simp add: injection_handler_returnOk ccorres_invocationCatch_Inr
                                             performInvocation_def)
                            apply (ctac add: setThreadState_ccorres)
                              apply csymbr
                              apply csymbr
                              apply (ctac(no_vcg) add: invokeTCB_ThreadControl_ccorres)
                                apply simp
                                apply (rule ccorres_alternative2)
                                apply (rule ccorres_return_CE, simp+)[1]
                               apply (rule ccorres_return_C_errorE, simp+)[1]
                              apply wp
                             apply simp
                             apply (wp sts_invs_minor')
                            apply (vcg exspec=setThreadState_modifies)
                           apply simp
                           apply (rule ccorres_split_throws, rule ccorres_return_C_errorE, simp+)
                           apply vcg
                          apply simp
                          apply (wp hoare_drop_imps)[1]
                         apply (wp injection_wp_E [OF refl])
                        apply (simp add: Collect_const_mem cintr_def intr_and_se_rel_def
                                         all_ex_eq_helper syscall_error_rel_def
                                         exception_defs)
                        apply (vcg exspec=deriveCap_modifies)
                       apply (simp cong: if_cong)
                       apply wp
                      apply (simp add: Collect_const_mem all_ex_eq_helper)
                      apply vcg
                     apply simp
                     apply (rule ccorres_split_throws, rule ccorres_return_C_errorE, simp+)
                     apply vcg
                    apply (simp cong: if_cong)
                    apply (wp hoare_drop_imps injection_wp_E[OF refl])
                   apply (simp add: Collect_const_mem all_ex_eq_helper
                                    numeral_eqs syscall_error_rel_def
                                    exception_defs cintr_def intr_and_se_rel_def)
                   apply (vcg exspec=deriveCap_modifies)
                  apply (simp cong: if_cong)
                  apply wp
                 apply (simp add: Collect_const_mem all_ex_eq_helper
                                  numeral_eqs syscall_error_rel_def
                                  exception_defs cintr_def intr_and_se_rel_def
                                  hd_drop_conv_nth2
                            cong: if_cong)
                 apply vcg
                apply (simp cong: if_cong)
                apply (wp hoare_drop_imps)
               apply (simp add: Collect_const_mem)
               apply (vcg exspec=slotCapLongRunningDelete_modifies)
              apply (simp cong: if_cong)
              apply (wp hoare_drop_imps)
             apply (simp add: Collect_const_mem all_ex_eq_helper
                              numeral_eqs syscall_error_rel_def
                              exception_defs cintr_def intr_and_se_rel_def)
             apply (vcg exspec=slotCapLongRunningDelete_modifies)
            apply (simp add: pred_conj_def cong: if_cong)
            apply (strengthen if_n_updateCapData_valid_strg)
            apply (wp hoare_drop_imps)
           apply (simp add: Collect_const_mem all_ex_eq_helper
                            numeral_eqs syscall_error_rel_def
                            exception_defs cintr_def intr_and_se_rel_def)
           apply vcg
          apply simp
          apply (wp hoare_drop_imps)
         apply (simp add: Collect_const_mem all_ex_eq_helper
                          numeral_eqs syscall_error_rel_def
                          exception_defs cintr_def intr_and_se_rel_def)
         apply vcg
        apply simp
        apply (wp hoare_drop_imps)
       apply (simp add: Collect_const_mem all_ex_eq_helper
                        numeral_eqs syscall_error_rel_def
                        exception_defs cintr_def intr_and_se_rel_def
                  cong: if_cong
                | vcg exspec=getSyscallArg_modifies
                | wp)+
  apply (clarsimp simp: if_1_0_0 word_less_nat_alt)
  apply (rule conjI)
   apply (clarsimp simp: ct_in_state'_def interpret_excaps_test_null
                         excaps_map_def neq_Nil_conv)
   apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def)
   apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def)
   apply (rule conjI, clarsimp simp: sysargs_rel_n_def n_msgRegisters_def)
   apply (auto simp: isCap_simps valid_tcb_state'_def
              elim!: st_tcb'_weakenE
              dest!: st_tcb_at_idle_thread' interpret_excaps_eq)[1]
  apply (clarsimp simp: linorder_not_le interpret_excaps_test_null
                        excaps_map_def neq_Nil_conv word_sle_def
                        word_sless_def)
  apply (frule interpret_excaps_eq[rule_format, where n=0], simp)
  apply (frule interpret_excaps_eq[rule_format, where n=1], simp)
  apply (clarsimp simp: mask_def[where n=4] ccap_rights_relation_def
                        rightsFromWord_wordFromRights
                        capTCBPtr_eq tcb_ptr_to_ctcb_ptr_mask
                        tcb_cnode_index_defs size_of_def
                        option_to_0_def rf_sr_ksCurThread
                        "StrictC'_thread_state_defs" mask_eq_iff_w2p word_size)
  apply (simp add: word_sle_def cap_get_tag_isCap)
  apply (subgoal_tac "args \<noteq> []")
   apply (clarsimp simp: hd_conv_nth)
   apply (drule sym, simp, simp add: true_def from_bool_0)
   apply clarsimp
   apply fastforce
  apply clarsimp
  done

lemma decodeTCBInvocation_ccorres:
  "interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
   ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple
              and valid_cap' cp and cte_at' slot and K (isThreadCap cp)
              and (excaps_in_mem extraCaps o ctes_of)
              and tcb_at' (capTCBPtr cp) and ex_nonz_cap_to' (capTCBPtr cp)
              and (\<lambda>s. \<forall>v \<in> set extraCaps. \<forall>y \<in> zobj_refs' (fst v).
                              ex_nonz_cap_to' y s)
              and (\<lambda>s. \<forall>v \<in> set extraCaps.
                             s \<turnstile>' fst v \<and> cte_at' (snd v) s)
              and (\<lambda>s. \<forall>v \<in> set extraCaps.
                             ex_cte_cap_wp_to' isCNodeCap (snd v) s)
              and sysargs_rel args buffer)
       (UNIV
            \<inter> {s. label_' s = label}
            \<inter> {s. ccap_relation cp (cap_' s)}
            \<inter> {s. unat (length_' s) = length args}
            \<inter> {s. slot_' s = cte_Ptr slot}
            \<inter> {s. extraCaps_' s = extraCaps'}
            \<inter> {s. call_' s = from_bool isCall}
            \<inter> {s. buffer_' s = option_to_ptr buffer}) []
     (decodeTCBInvocation label args cp slot extraCaps
            >>= invocationCatch thread isBlocking isCall InvokeTCB)
     (Call decodeTCBInvocation_'proc)"
  apply (cinit' lift: label_' cap_' length_' slot_' extraCaps_' call_' buffer_')
   apply (simp add: decodeTCBInvocation_def invocation_eq_use_types
               del: Collect_const)
   apply (rule ccorres_Cond_rhs)
    apply simp
    apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeReadRegisters_ccorres [where buffer=buffer])
      apply (rule ccorres_return_CE, simp+)[1]
     apply (rule ccorres_return_C_errorE, simp+)[1]
    apply wp
   apply (rule ccorres_Cond_rhs)
    apply simp
    apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeWriteRegisters_ccorres [where buffer=buffer])
      apply (rule ccorres_return_CE, simp+)[1]
     apply (rule ccorres_return_C_errorE, simp+)[1]
    apply wp
   apply (rule ccorres_Cond_rhs)
    apply simp
    apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeCopyRegisters_ccorres [where buffer=buffer])
      apply (rule ccorres_return_CE, simp+)[1]
     apply (rule ccorres_return_C_errorE, simp+)[1]
    apply wp
   apply (rule ccorres_Cond_rhs)
    apply (simp add: returnOk_bind ccorres_invocationCatch_Inr)
    apply (rule ccorres_rhs_assoc)+
    apply (ctac add: setThreadState_ccorres)
      apply csymbr
      apply (simp add: performInvocation_def)
      apply (ctac add: invokeTCB_Suspend_ccorres)
         apply simp
         apply (rule ccorres_alternative2)
         apply (rule ccorres_return_CE, simp+)[1]
        apply (rule ccorres_return_C_errorE, simp+)[1]
       apply wp
      apply (vcg exspec=invokeTCB_Suspend_modifies)
     apply (wp sts_invs_minor')
    apply (vcg exspec=setThreadState_modifies)
   apply (rule ccorres_Cond_rhs)
    apply (simp add: returnOk_bind ccorres_invocationCatch_Inr)
    apply (rule ccorres_rhs_assoc)+
    apply (ctac add: setThreadState_ccorres)
      apply csymbr
      apply (simp add: performInvocation_def)
      apply (ctac add: invokeTCB_Resume_ccorres)
         apply simp
         apply (rule ccorres_alternative2)
         apply (rule ccorres_return_CE, simp+)[1]
        apply (rule ccorres_return_C_errorE, simp+)[1]
       apply wp
      apply (vcg exspec=invokeTCB_Resume_modifies)
     apply (wp sts_invs_minor')
    apply (vcg exspec=setThreadState_modifies)
   apply (rule ccorres_Cond_rhs)
    apply simp
    apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeTCBConfigure_ccorres [where buffer=buffer])
      apply (rule ccorres_return_CE, simp+)[1]
     apply (rule ccorres_return_C_errorE, simp+)[1]
    apply wp
   apply (rule ccorres_Cond_rhs)
    apply simp
    apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeSetPriority_ccorres [where buffer=buffer])
      apply (rule ccorres_return_CE, simp+)[1]
     apply (rule ccorres_return_C_errorE, simp+)[1]
    apply wp
   apply (rule ccorres_Cond_rhs)
    apply simp
    apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeSetIPCBuffer_ccorres [where buffer=buffer])
      apply (rule ccorres_return_CE, simp+)[1]
     apply (rule ccorres_return_C_errorE, simp+)[1]
    apply wp
   apply (rule ccorres_Cond_rhs)
    apply simp
    apply (rule ccorres_add_returnOk, ctac(no_vcg) add: decodeSetSpace_ccorres [where buffer=buffer])
      apply (rule ccorres_return_CE, simp+)[1]
     apply (rule ccorres_return_C_errorE, simp+)[1]
    apply wp
   apply (rule ccorres_equals_throwError)
    apply (fastforce simp: throwError_bind invocationCatch_def
                   split: invocation_label.split)
   apply (simp add: ccorres_cond_iffs
              cong: StateSpace.state.fold_congs globals.fold_congs)
   apply (rule syscall_error_throwError_ccorres_n)
   apply (simp add: syscall_error_to_H_cases)
  apply (clarsimp simp: cintr_def intr_and_se_rel_def
                        exception_defs rf_sr_ksCurThread
                        Collect_const_mem)
  apply (rule conjI)
   apply (auto simp: ct_in_state'_def isCap_simps valid_tcb_state'_def
              elim!: st_tcb'_weakenE
              dest!: st_tcb_at_idle_thread')[1]
  apply (simp split: sum.split add: cintr_def intr_and_se_rel_def
                        exception_defs syscall_error_rel_def)
  apply (simp add: "StrictC'_thread_state_defs" mask_eq_iff_w2p word_size
                   cap_get_tag_isCap)
  apply (simp add: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H)
  apply clarsimp
  done

end
end
